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

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

【參考文獻】

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

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

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

，

本文編號：1995490