發(fā)布時(shí)間：2018-06-08 10:30

  本文選題：可能的Kripke結(jié)構(gòu) + 可能性測(cè)度��； 參考：《陜西師范大學(xué)》2013年碩士論文

【摘要】：模型檢測(cè)技術(shù)因其具有簡(jiǎn)潔明了,自動(dòng)化程度高等優(yōu)點(diǎn),被應(yīng)用于工業(yè)設(shè)計(jì)的諸多領(lǐng)域,特別是硬件系統(tǒng)、軟件系統(tǒng).這種基于仿真、測(cè)試、演繹和推理的自動(dòng)驗(yàn)證技術(shù)作為一種形式化的方法和工具,可以有效地檢測(cè)到硬件和軟件系統(tǒng)存在的風(fēng)險(xiǎn)和漏洞,這種技術(shù)在近二十年得到了極大的發(fā)展,從經(jīng)典的模型檢測(cè)到概率模型檢測(cè)再到如今的可能性測(cè)度下的模型檢測(cè),無(wú)數(shù)的專家和學(xué)者對(duì)這種形式化的自動(dòng)驗(yàn)證技術(shù)無(wú)論是在理論上還是應(yīng)用上做出了巨大的貢獻(xiàn).經(jīng)典的模型檢測(cè)技術(shù)要求系統(tǒng)模型及性質(zhì)必須是精確無(wú)異義的,然而現(xiàn)實(shí)世界無(wú)論是從信息的獲取還是信息的描述,往往都具有不確定性,這種不確定性既包括概率不確定性,也包括模糊不確定性,2008年,Baier和Katoen以有窮的馬爾可夫鏈(Markov Chain)為概率系統(tǒng)的模型,建立了基于概率測(cè)度的模型檢測(cè)的原理和方法,這使得模型檢測(cè)在技術(shù)和理論上都極大地提高了一個(gè)層面,也使得模型檢測(cè)的應(yīng)用面更加的廣泛.自從Zadeh提出了模糊集的概念后,模糊數(shù)學(xué)成為數(shù)學(xué)領(lǐng)域又一個(gè)刻畫(huà)不確定性的經(jīng)典理論,而模糊數(shù)學(xué)最重要的應(yīng)用領(lǐng)域之一就是計(jì)算智能.因此,模糊環(huán)境下的模型檢測(cè)技術(shù)的研究對(duì)于計(jì)算機(jī)科學(xué)理論的發(fā)展具有十分重要的意義.本文即是在這方面的一個(gè)嘗試,將可能性測(cè)度與模型檢測(cè)相結(jié)合建立了一些基于可能性測(cè)度的模型檢測(cè)的定義和定理等. 在經(jīng)典模型檢測(cè)理論中當(dāng)狀態(tài)數(shù)以指數(shù)的形式增加時(shí),就會(huì)發(fā)生狀態(tài)爆炸,然而在模糊環(huán)境下,由于對(duì)狀態(tài)的刻畫(huà)模糊化,所以系統(tǒng)所承受的壓力會(huì)更大,同時(shí)發(fā)生狀態(tài)爆炸的幾率也會(huì)增高.因?yàn)榛ツ�擬可以有效地化簡(jiǎn)狀態(tài)數(shù)從而將復(fù)雜的分支結(jié)構(gòu)簡(jiǎn)化,所以在經(jīng)典的模型檢測(cè)技術(shù)中,互模擬作為一種抑制狀態(tài)爆炸的重要方法.為了解決可能性測(cè)度下的狀態(tài)爆炸的問(wèn)題,可能性測(cè)度下互模擬的研究就顯得十分的重要. 花費(fèi)問(wèn)題在一些分析決策系統(tǒng)中被作為關(guān)注的重點(diǎn).Baier和Katoen又以有窮的馬爾可夫鏈作為概率系統(tǒng)的模型系統(tǒng)地介紹了概率花費(fèi)的概念,特別是對(duì)于概率可達(dá)花費(fèi)問(wèn)題作了詳細(xì)的介紹.本文則是在可能性測(cè)度下作了一些嘗試,初步建立了基于可能性測(cè)度的可能性花費(fèi)的概念,給出了相關(guān)結(jié)論. 本文主要工作如下： (1)基于可能的Kripke結(jié)構(gòu),在計(jì)算樹(shù)邏輯和概率計(jì)算樹(shù)邏輯的基礎(chǔ)上提出了基于可能性測(cè)度的可能性計(jì)算樹(shù)邏輯(PoCTL*),可能性計(jì)算樹(shù)邏輯(PoCTL-)的相關(guān)概念. (2)在經(jīng)典互模擬和可能性測(cè)度的基礎(chǔ)上建立了可能性互模擬的相關(guān)定義,給出了對(duì)于兩個(gè)滿足可能性互模擬的可能的Kripke結(jié)構(gòu)的相互表示以及可能性互模擬的化簡(jiǎn).證明了可能性互模擬滿足自反性、對(duì)稱性和傳遞性,以及可能性互模擬的跡相等、可能性互模擬閉包事件�？赡苄缘刃再|(zhì).又證明了(PoCTL)等價(jià)、(PoCTL*)等價(jià)和(PoCTL-)等價(jià)與可能性互模擬等價(jià)的相互關(guān)系. (3)對(duì)可能性花費(fèi)問(wèn)題進(jìn)行了相關(guān)的討論,建立了基于可能性測(cè)度的可能性花費(fèi)模型,可能性花費(fèi)計(jì)算樹(shù)邏輯(PoRCTL)的語(yǔ)構(gòu)定義等.
[Abstract]:Since Zadeh proposed the concept of fuzzy set , the research of model detection technology based on simulation , testing , deduction and reasoning is very important to the development of computer science theory .

In the classical model detection theory , when the state numbers increase exponentially , the state explosion occurs . However , under the fuzzy environment , the pressure of the system can be increased , and the probability of state explosion can be increased . Because the mutual simulation can effectively reduce the number of states and simplify the complex branch structure , in the classical model detection technology , the mutual simulation is an important method to suppress the state explosion . In order to solve the problem of state explosion under the probability measure , the research on the mutual simulation under the possibility measure is very important .

In this paper , the concept of probability cost is systematically introduced in Baier and Katoen as the model of probability system . In this paper , some attempts have been made on probability measure , and the concept of probability measure based on probability measure is preliminarily established , and relevant conclusions are given .

The main work of this paper is as follows :

( 1 ) Based on the possible Kripke structure , a possibility calculating tree logic ( PoCTL * ) based on probability measure is proposed on the basis of calculating tree logic and probability calculation tree logic , and the related concept of probability calculation tree logic ( PoCTL - ) is proposed .

( 2 ) On the basis of classical mutual simulation and possibility measure , a correlative definition of possibility cross - simulation is established , and the mutual representation of possible Kripke structures and the mutual simulation of possibility are given .

( 3 ) the possibility cost problem is discussed , the possibility cost model based on possibility measure is established , and the language definition of the tree logic ( PoRCTL ) is expended .
【學(xué)位授予單位】：陜西師范大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2013
【分類號(hào)】：TP306;O211

【參考文獻(xiàn)】

相關(guān)期刊論文 前2條

1 趙林;吳盡昭;;基于吳方法的多值模型檢驗(yàn)[J];系統(tǒng)科學(xué)與數(shù)學(xué);2008年08期

2 雷麗暉;段振華;;使用擴(kuò)展區(qū)間時(shí)序邏輯為并發(fā)工作流建模[J];西安電子科技大學(xué)學(xué)報(bào);2007年04期

，

本文編號(hào)：1995490