摘要
Thispaperinvestigatessymbolicalgorithmicanalysisofrectangularhybridsystems.Todealwiththesymbolicreachabilityproblem,arestrictedconstraintsystemcalledhybridzoneisformalizedfortherepresentationandmanipulationofrectangularautomatastate-spaces.Hybridzonesareprovedtobeclosedoversymbolicreachabilityoperationsofrectangularhybridsystems.Theyarealsoappliedtomodel-checkingproceduresforverifyingsomeimportantclassesoftimedcomputationtreelogicformulas.Torepresenthybridzones,adatastructurecalleddifferenceconstraintmatrixisdefined.Theseenableustodealwiththesymbolicalgorithmicanalysisofrectangularhybridsystemsinanefficientway.
出版日期
2009年03月13日(中国期刊网平台首次上网日期,不代表论文的发表时间)