基于混合时序逻辑的混合系统的模型检测 (1)

《基于混合时序逻辑的混合系统的模型检测 (1)》由会员上传分享，免费在线阅读，更多相关内容在工程资料-天天文库。

1、h基于混合时序逻辑的混合系统的模型检测#张海宾*（西安电子科技大学计算机学院，西安，710071）510152025303540摘要：这篇文章处理基于混合时序逻辑的混合系统的模型检测技术。通过转换为区间时序逻辑的模型检测问题我们解决了时间自动机的模型检测问题。然后通过转换为时间自动机的模型检测问题，解决了多速率混合系统的模型检测问题。最后，我们给出了矩形混合系统基于线性命题逻辑的模型检测算法。关键词：混合系统；时序逻辑；混合系统中图分类号：TP31ModelCheckingHybridSystemsWi

2、thinHybridTemporalLogicZHANGHaibin(SchoolofComputerScienceandTechnology,XidianUniversity,xi'an,710071)Abstract:Inthispaper,wedealwiththemodelcheckingissueforhybridsystemswithinhybridtemporallogic.Wesolvethemodelcheckingproblemfortimedautomatabytranslatingi

3、ttothesameissueforintervaltemporallogic.Thenweprovethatthemodelcheckingissueofmultirateautomatacanbetranslatedtothatoftimedautomata.Finally,wegiveanapproachforcheckingthelinearpropositionalpropertyofcompactrectangularautomata.Keywords:modelchecking；tempora

4、llogic；hybridsystems０.IntroductionIntervalTemporalLogic(ITL)[1]isanimportantclassoftemporallogic.ThesatisfiabilityproblemforITLinterpretedoverinfinitemodelwassolvedin[2].Thus,themodelcheckingITLproblemcanbesolvedtoo.Hybridsystems[3-5]arereal-timesystemsconsi

5、stingofanon-trivialmixtureofcontinuousactivitiesanddiscreteevents.Itisverydifficulttoverifyhybridsystemsevenfortheveryrestrictedclasses.Thereachabilityproblemofsubclassesofhybridsystems—timed,multirateandcompactrectangularautomatawereprovedtobedecidable[3].

6、Inthispaper,wedealwithmodelcheckingproblemswithinHybridTemporalLogic[6](HTL)fortimed,multirateandcompactrectangularautomata.Tothisend,weuseasubsetofHTLtodescribetherequirementsspecificationofasystem.TocheckwhetheratimedautomataMsatisfiesanHTLformulaj(i.e.M=j

7、),weconstructaLabelledBuchiAutomata(LBA)M'forMandanITLformulajforj,andprovethatM=jifandonlyifM'=s,whichisaproblemofmodelcheckingITLwhichcanbesolved.Besides,therationalmodelcheckingproblemfortimedautomataisdealtwithsimilarly.Thenweverifythemultirateautomata

8、byprovingthatitisisomorphicbetweencheckingmultirateautomataandtimedautomata.Finally,wehaveaprimaryattemptforcheckingtherectangularautomata,tocheckthelinearpropositionalpropertyfortherestrictedrectangularautom