廣義可能性計(jì)算樹邏輯的范式研究

ID:35076498

大小:2.72 MB

頁(yè)數(shù):47頁(yè)

時(shí)間:2019-03-17

廣義可能性計(jì)算樹邏輯的范式研究_第1頁(yè)
廣義可能性計(jì)算樹邏輯的范式研究_第2頁(yè)
廣義可能性計(jì)算樹邏輯的范式研究_第3頁(yè)
廣義可能性計(jì)算樹邏輯的范式研究_第4頁(yè)
廣義可能性計(jì)算樹邏輯的范式研究_第5頁(yè)
資源描述:

《廣義可能性計(jì)算樹邏輯的范式研究》由會(huì)員上傳分享,免費(fèi)在線閱讀,更多相關(guān)內(nèi)容在學(xué)術(shù)論文-天天文庫(kù)

1、分類號(hào)TP301.2密級(jí)公開學(xué)號(hào)132275■■■^arnsuga碩it學(xué)位論文(學(xué)術(shù)型)題目廣義可能性計(jì)算樹邏輯的范式研究作者趙杰指導(dǎo)教師李永明教授-級(jí)學(xué)科名稱計(jì)算機(jī)科學(xué)與技術(shù)二級(jí)學(xué)科名稱計(jì)算機(jī)系統(tǒng)結(jié)構(gòu)提交日期二〇—六年五月學(xué)位論文原創(chuàng)性聲明本人聲明所呈交的學(xué)位論文是我在導(dǎo)師的指導(dǎo)下進(jìn)行研巧工作所取巧的研巧成果?盡我所知,除文中己經(jīng)注明引用的內(nèi)容和致謝的地方外,本論文不包含其他個(gè)人或集體已經(jīng)發(fā)表或揉寫過(guò)的研巧成果,也不包含本人或他人已申請(qǐng)學(xué)位或其他用途

2、使用過(guò)的成果?對(duì)本文的研巧做出重要貢獻(xiàn)的個(gè)人和集體,巧已在文中作了明確說(shuō)明并表示謝意。一本學(xué)位論文若有不實(shí)或者侵犯他人權(quán)利的,本人應(yīng)意承擔(dān)切相關(guān)的法律責(zé)任。扛>G?作者k曰期:/(年月>曰學(xué)位論文知識(shí)產(chǎn)權(quán)及使用授權(quán)聲明書本人在導(dǎo)師指導(dǎo)下所完成的學(xué)位論文及相關(guān)成果,知識(shí)產(chǎn)權(quán)歸屬陜西師范大學(xué)。本人完全了解陜西師范大學(xué)有關(guān)保存、使用學(xué)位論文的規(guī)忠允許本論文被査閱和借閱,學(xué)校有權(quán)保留學(xué)位論文并向國(guó)家有關(guān)部口或機(jī)構(gòu)送交論文的紙質(zhì)版和電子版,有權(quán)將本論文的全部或部分內(nèi)容編入有關(guān)數(shù)據(jù)庫(kù)進(jìn)行檢索,可W采用。本人

3、保證畢業(yè)離校后任何復(fù)制手段保存和匯編本論文,發(fā)表本論文或使用本論文成果時(shí)署名單位仍為陜西師范大學(xué)?保密論文解密后適用本聲明。作者簽名:fc去、日巧:>。11年^月X日摘要1981a一自從年Clrk和Emerson提出了模型檢測(cè),其作為種形式化的自動(dòng)化驗(yàn)證技術(shù)有效的彌補(bǔ)了傳統(tǒng)測(cè)試方案所遺留的問(wèn)題,因此受到了人們的普遍的一般過(guò)程是這樣的關(guān)注。模型檢測(cè)的:首先對(duì)需要被檢測(cè)的系統(tǒng)和被驗(yàn)證的性質(zhì)進(jìn)行抽象建模,再通過(guò)模型檢測(cè)算法對(duì)模型進(jìn)行形式化驗(yàn)證來(lái)判斷系統(tǒng)是否滿足對(duì)應(yīng)的性質(zhì)。,在經(jīng)典的模型檢測(cè)理論中,由于無(wú)法

4、正確的處理系統(tǒng)的中不確定性問(wèn)題因一此些學(xué)者提出了多種狀態(tài)遷移的量化擴(kuò)展,基于廣義可能性Kripke結(jié)構(gòu)的廣一個(gè)代表義可能性計(jì)算樹還輯的模型檢測(cè)就是其中的。由于時(shí)序邏輯的范式在模型檢測(cè)中有著重要的應(yīng)用,但是在廣義可能性計(jì)算樹邏輯中還沒有對(duì)范式進(jìn)行過(guò)系統(tǒng)的研充,因此本文的主要工作就是在此背景下進(jìn)行的。本文的主要內(nèi)容如下:1一一正態(tài)范式.本文給出了廣義可能性計(jì)算樹邏輯的兩種不同的范式PositiveNormalForm,簡(jiǎn)記為PNF和存在范式ExistentialNormalForm,簡(jiǎn)記為()(EN巧,

5、并且給出了對(duì)應(yīng)范式的語(yǔ)構(gòu)和語(yǔ)義解釋。一2.通過(guò)歸納假設(shè)法證明了對(duì)于任意的個(gè)廣義可能性計(jì)算樹邏溝的公式都存在與之等價(jià)的PNF和ENF的公式。3一.給出了個(gè)將任意的廣義可能性計(jì)算樹邏輯的公式轉(zhuǎn)換為與之對(duì)應(yīng)的PNF公式巧ENF公式的算法,并且通過(guò)實(shí)例進(jìn)行分析說(shuō)明。,廣義可能性,關(guān)鍵詞,計(jì)算樹邏輯范式:模型檢測(cè)IAbstractSinceClarkandEmersonintroducedthenotonofmodelcheckn191tiingi8i,hasbeenwidelycon

6、cernedforthereasonthatmodelchecking,asakindofformala山omaticverification化chnoocansolvetherobemsleerelgy,plftovfromthtraditionall:estinmethod.Theeneralstesofmodelcheckinincludeabstractnggpgigthearoriatemodelof化ecurrentss化manddescri

7、bintheverifiedroertiespppygpp,thendeterminingwhetherthesstemsatisfiestheroertiesornotbthemeansofyppymodelcheckinaorthms.glgiIntheclassicaltheoryofmodelcheckingthereasonthattheuncertaint,byyproblemscannotbesolvedsuccessfully,some

8、scholarsputforwardkindsofuantitatiiveextensionsof化etransito打sstemoneofwhich

當(dāng)前文檔最多預(yù)覽五頁(yè),下載文檔查看全文

此文檔下載收益歸作者所有

當(dāng)前文檔最多預(yù)覽五頁(yè),下載文檔查看全文
溫馨提示:
1. 部分包含數(shù)學(xué)公式或PPT動(dòng)畫的文件,查看預(yù)覽時(shí)可能會(huì)顯示錯(cuò)亂或異常,文件下載后無(wú)此問(wèn)題,請(qǐng)放心下載。
2. 本文檔由用戶上傳,版權(quán)歸屬用戶,天天文庫(kù)負(fù)責(zé)整理代發(fā)布。如果您對(duì)本文檔版權(quán)有爭(zhēng)議請(qǐng)及時(shí)聯(lián)系客服。
3. 下載前請(qǐng)仔細(xì)閱讀文檔內(nèi)容,確認(rèn)文檔內(nèi)容符合您的需求后進(jìn)行下載,若出現(xiàn)內(nèi)容與標(biāo)題不符可向本站投訴處理。
4. 下載文檔時(shí)可能由于網(wǎng)絡(luò)波動(dòng)等原因無(wú)法下載或下載錯(cuò)誤,付費(fèi)完成后未能成功下載的用戶請(qǐng)聯(lián)系客服處理。
关闭