資源描述:
《廣義可能線性時序邏輯的自動機(jī)方法》由會員上傳分享,免費在線閱讀,更多相關(guān)內(nèi)容在學(xué)術(shù)論文-天天文庫。
1、分類號TP301.2密級公開學(xué)^132267■■■1誦顆,U!誦腦腳■碩:Jr?qū)W位論文(學(xué)術(shù)型)題目廣義可能線性時序邏輯的自動機(jī)方法作者指導(dǎo)教師李永明教授-級學(xué)科名稱計算機(jī)科學(xué)與技術(shù)二級學(xué)科名稱計算機(jī)軟件與理論提交日期二〇—六年六月陜西師范大學(xué)學(xué)位論文獨創(chuàng)性聲明本人聲明所呈交的學(xué)位論文是我在導(dǎo)師的指導(dǎo)下進(jìn)行研究工作所取得的研巧成果。盡我所知,除文中已經(jīng)注明引用的內(nèi)容和致謝的地方外,本論文不包含其他個人或集體已經(jīng)發(fā)表或撰寫過的研究成果,也不包含本人或他人已申請學(xué)位或其他用途使用過的
2、成果。對本文的研巧做出重要貢獻(xiàn)的個人和集體,均已在文中。本學(xué)位論文若有不實或者侵犯他人權(quán)利的作了明確說明并表示謝意,本人愿意一承擔(dān)切相關(guān)的法律責(zé)任。作者簽名:日期;陜西師范大學(xué)學(xué)位論文使用授權(quán)聲明本人在導(dǎo)師指導(dǎo)下所完成的學(xué)位論文及相關(guān)成果,知識產(chǎn)權(quán)歸屬陜西師范大學(xué)。本人完全了解陜西師范大學(xué)有關(guān)保存、使用學(xué)位論文的規(guī)定,允許本論文被查閱和借閱,學(xué)校有權(quán)保留學(xué)位論文并向國家有關(guān)部口或機(jī)構(gòu)送交論文的紙質(zhì)版,和電子版,有權(quán)將本論文的全部或部分內(nèi)容編入有關(guān)數(shù)據(jù)庫進(jìn)行檢索可W采用任何復(fù)制手段保存和匯編本論文。本人保證畢業(yè)離校后,發(fā)表本論文或
3、使用本論文成果時署名單位仍為陜西師范大學(xué)。保密論文解密后適用本聲明。作者簽名;:制本日期呈iLLZr摘要一98模型檢測是針對有窮狀態(tài)系統(tǒng)的種可1^自動驗證的技術(shù)。早在11年,相繼由Clarke、Emerson、Quielle和Sifakis提出。模型檢測基本模型是遷移系統(tǒng),經(jīng)典模型檢測針對的是定性的系統(tǒng),隨著計算機(jī)軟硬件日趨復(fù)雜化,在遷移系統(tǒng)中會存在很多不確定的信息。為了解決這些不確定的信息所帶來的問題,學(xué)者們,將狀態(tài)遷移模型進(jìn)行量化擴(kuò)展,比如狀態(tài)中加入時間因素或在模型中加入概率、,Zadeh提出模糊集理論可能性或統(tǒng)計。在19
4、化年,隨后模糊可能測度得到了廣泛的研究。最近,李永明提出基于廣義可能性測度模型檢測。本文研究的內(nèi)容是是廣義可能模型檢測和自動機(jī)理論與基礎(chǔ)的一個交叉方向一的內(nèi)容,線性時序邏輯模型檢測的個重要方法就是將線性時序邏輯公式轉(zhuǎn)化為B社沈i自動機(jī),并用自動機(jī)的相關(guān)結(jié)果給出對應(yīng)模型檢測算法。雖然針對廣義可能性測度下的線性時序邏輯模型檢測己有研究,但是如何將廣義可能線性時序邏,輯公式轉(zhuǎn)化為Bikh,i自動機(jī)這方面還沒有得到研巧本文給出了廣義可能線性時序邏輯公式的模糊交替Bii油i自動機(jī)和模糊Biichi自動機(jī)方法,并給出對應(yīng)的廣j義可能線性時序邏
5、轅模型檢測方法和算法復(fù)雜度分析.本文主要工作如下:1.^首先,給出了線性時序邏輯語構(gòu)和語義,廣義可能Kripke結(jié)構(gòu)模型式及相關(guān)性質(zhì)概念。2.其次,分別介紹了交替Bii油i自動機(jī)、非確定性Bikhi自動機(jī)、模糊交替Biichi自動機(jī)和模糊Bikhi自動機(jī)W及交替Bii油i自動機(jī)和非確定性Biichi自動機(jī)模型檢測方法。3.最后,在廣義可能線性時序邏輯語構(gòu)和語義基礎(chǔ)上,給出了模糊交替B扣hi自動機(jī)和模糊Biichi自動機(jī)方法,并予W證明。在廣義可能測度下,給出了廣義可能線性時序邏輯模型檢測方法,進(jìn)而給出對應(yīng)的算法復(fù)雜度分析。關(guān)鍵
6、巧:模型檢測,自動機(jī),Biichi自動機(jī),線性時序邏揖,交替自動機(jī)、AbstractModei行esthesstemswithfi打itestatesa打ditcanexecuteau-lchecki打gverytomatica.ithetitittllThemodelofmodelcheckhigsrai化onsstemandheheyy,classicalmodelcheckingsystemisqualitative.W化hthedevelopmentofcomputer
7、hardwareandsoftwaretherewillbealotofuncertaininformationinthetransition,*system.I打ordertosolvetheproblemscausedbytheunceitai打informatio打the,researchershaveextendedthestatestransitionsystem.Forexampleaddintime,gfactori打thestatesoroi打inrobabi