資源描述：
《基于混合時(shí)序邏輯的混合系統(tǒng)的模型檢測》由會員上傳分享，免費(fèi)在線閱讀，更多相關(guān)內(nèi)容在工程資料-天天文庫。
1、h基于混合時(shí)序邏輯的混合系統(tǒng)的模型檢測#張海賓*（西安電子科技大學(xué)計(jì)算機(jī)學(xué)院，西安，710071）510152025303540摘要：這篇文章處理基于混合時(shí)序邏輯的混合系統(tǒng)的模型檢測技術(shù)。通過轉(zhuǎn)換為區(qū)間時(shí)序邏輯的模型檢測問題我們解決了時(shí)間自動機(jī)的模型檢測問題。然后通過轉(zhuǎn)換為時(shí)間自動機(jī)的模型檢測問題，解決了多速率混合系統(tǒng)的模型檢測問題。最后，我們給出了矩形混合系統(tǒng)基于線性命題邏輯的模型檢測算法。關(guān)鍵詞：混合系統(tǒng)；時(shí)序邏輯；混合系統(tǒng)中圖分類號：TP31ModelCheckingHybridSystemsWithinHybridTemporalLogicZH
2、ANGHaibin(SchoolofComputerScienceandTechnology,XidianUniversity,xi'an,710071)Abstract:Inthispaper,wedealwiththemodelcheckingissueforhybridsystemswithinhybridtemporallogic.Wesolvethemodelcheckingproblemfortimedautomatabytranslatingittothesameissueforintervaltemporallogic.Thenweprov
3、ethatthemodelcheckingissueofmultirateautomatacanbetranslatedtothatoftimedautomata.Finally,wegiveanapproachforcheckingthelinearpropositionalpropertyofcompactrectangularautomata.Keywords:modelchecking；temporallogic；hybridsystems０.IntroductionIntervalTemporalLogic(ITL)[1]isanimportan
4、tclassoftemporallogic.Thesatis?abilityproblemforITLinterpretedoverin?nitemodelwassolvedin[2].Thus,themodelcheckingITLproblemcanbesolvedtoo.Hybridsystems[3-5]arereal-timesystemsconsistingofanon-trivialmixtureofcontinuousactivitiesanddiscreteevents.Itisverydif?culttoverifyhybridsyst
5、emsevenfortheveryrestrictedclasses.Thereachabilityproblemofsubclassesofhybridsystems—timed,multirateandcompactrectangularautomatawereprovedtobedecidable[3].Inthispaper,wedealwithmodelcheckingproblemswithinHybridTemporalLogic[6](HTL)fortimed,multirateandcompactrectangularautomata.T
6、othisend,weuseasubsetofHTLtodescribetherequirementsspeci?cationofasystem.TocheckwhetheratimedautomataMsatis?esanHTLformulaj(i.e.M=j),weconstructaLabelledBuchiAutomata(LBA)M'forMandanITLformulajforj,andprovethatM=jifandonlyifM'=s,whichisaproblemofmodelcheckingITLwhichcanbesolved.Be
7、sides,therationalmodelcheckingproblemfortimedautomataisdealtwithsimilarly.Thenweverifythemultirateautomatabyprovingthatitisisomorphicbetweencheckingmultirateautomataandtimedautomata.Finally,wehaveaprimaryattemptforcheckingtherectangularautomata,tocheckthelinearpropositionalpropert
8、yfortherestrictedrectangularautom
