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

【摘要】：在實(shí)際生活中,較大的和復(fù)雜的系統(tǒng)在運(yùn)行過(guò)程中不可避免地出現(xiàn)不確定的、不一致的信息,所以經(jīng)典的模型檢測(cè)不能處理并發(fā)系統(tǒng)中所有的驗(yàn)證問(wèn)題.為了處理概率不確定性的系統(tǒng)驗(yàn)證,Baier和Katoen介紹了基于概率測(cè)度的模型檢測(cè)的原理和方法,Hart和Sharir將概率論應(yīng)用于模型檢測(cè).而現(xiàn)實(shí)生活中有很多復(fù)雜的問(wèn)題不滿(mǎn)足概率測(cè)度下的可加性,這些問(wèn)題并不能用概率模型進(jìn)行驗(yàn)證,因此對(duì)非可加性測(cè)度下模型檢測(cè)的研究具有理論與實(shí)際意義.可能性測(cè)度是一種非可加性測(cè)度,基于可能性測(cè)度的線(xiàn)性時(shí)序邏輯(LTL)和計(jì)算樹(shù)邏輯(CTL)模型檢測(cè)已經(jīng)有一些重要的研究成果,但還有一些重要且關(guān)鍵的問(wèn)題尚未探討：可能性測(cè)度下瞬時(shí)測(cè)度是否存在,瞬時(shí)可能性測(cè)度與可達(dá)可能性測(cè)度的關(guān)系,計(jì)算樹(shù)邏輯和可能性測(cè)度下計(jì)算樹(shù)邏輯(PoCTL)的關(guān)系等,本文就針對(duì)這幾個(gè)問(wèn)題進(jìn)行探討. 論文主要做了以下兩方面的工作： (1)提出了瞬時(shí)可能性測(cè)度的概念,并用構(gòu)造法證明了在轉(zhuǎn)移步數(shù)限制下的可達(dá)可能性測(cè)度與可達(dá)瞬時(shí)可能性測(cè)度相等,受限的轉(zhuǎn)移步數(shù)限制下的可達(dá)可能性測(cè)度與受限可達(dá)瞬時(shí)可能性測(cè)度相等.探討了在可能性測(cè)度下并、交、補(bǔ)運(yùn)算成立的條件以及那些LTL性質(zhì)成立,特別是在強(qiáng)連通子集下重復(fù)可達(dá)事件和持久性事件的性質(zhì). (2)基于可能性測(cè)度對(duì)CTL做了進(jìn)一步的探討,給出了PoCTL公式與CTL公式和PoCTL公式與PoCTL公式分別等價(jià)的定義.利用公式的等價(jià)性證明了PoJ(φ)在非運(yùn)算下成立.對(duì)PoCTL中事件的可能性大于0以及等于1時(shí)的性質(zhì)做了詳細(xì)的探討,深入研究了PoCTL與CTL的異同,得出了CTL公式是PoCTL公式的一個(gè)真子集.對(duì)CTL公式中的重復(fù)事件和持久性事件的定性性質(zhì)和定量性質(zhì)進(jìn)行了詳細(xì)的研究,通過(guò)例子說(shuō)明了在可能性測(cè)度與概率測(cè)度下CTL公式的區(qū)別.最后給出了PoCTL模型檢測(cè)的步驟和時(shí)間復(fù)雜度,說(shuō)明了模型檢測(cè)的可行性.
[Abstract]:In real life, uncertain and inconsistent information is inevitable in large and complex systems, so classical model checking can not deal with all the verification problems in concurrent systems. In order to deal with probabilistic system verification, Baier and Katoen introduce the principle and method of model detection based on probability measure. Hart and Sharir apply probability theory to model detection. However, there are many complicated problems in real life that can not satisfy the additivity of probability measure, and these problems can not be verified by probability model. Therefore, the research on model detection under non-additive measure is of theoretical and practical significance. Possibility measure is a kind of non-additive measure. There have been some important research achievements in model detection of linear temporal logic (LTL) and computational tree logic (CTL) based on possibility measure. But there are still some important and key problems that have not been discussed: the existence of instantaneous measure under possibility measure, the relationship between instantaneous possibility measure and reachability measure, the relation between computing tree logic and computing tree logic PoCTL under possibility measure, etc. This paper discusses these problems. The main work of this paper is as follows: In this paper, the concept of instantaneous probability measure is proposed, and the method of construction is used to prove that the reachability measure is equal to the reachable instantaneous possibility measure under the limit of the number of transition steps. The measure of reachability under the restriction of the number of transfer steps is equal to the measure of the instantaneous probability of limited reachability. In this paper, we discuss the conditions for the union, intersection and complement operations to hold under the possibility measure, and the properties of those LTL properties, especially the repeated reachable events and persistent events under strongly connected subsets. 2) based on the possibility measure, the definition of PoCTL formula and CTL formula and PoCTL formula and PoCTL formula are given. By using the equivalence of the formula, it is proved that PoJ (蠁) holds in non-operation. In this paper, the possibility of events in PoCTL is discussed in detail, which is greater than 0 and equal to 1. The similarities and differences between PoCTL and CTL are deeply studied. It is concluded that the CTL formula is a true subset of PoCTL formula. The qualitative and quantitative properties of repeated events and persistent events in CTL formula are studied in detail. The difference between CTL formula under probability measure and possibility measure is illustrated by examples. Finally, the steps and time complexity of PoCTL model detection are given, and the feasibility of model detection is illustrated.
【學(xué)位授予單位】：陜西師范大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2013
【分類(lèi)號(hào)】：TP306;O211

【參考文獻(xiàn)】

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

1 徐蔚文,陸鑫達(dá);身份認(rèn)證協(xié)議的模型檢測(cè)分析[J];計(jì)算機(jī)學(xué)報(bào);2003年02期

2 鄧輝;薛艷;李亞利;李永明;;基于可能性測(cè)度的計(jì)算樹(shù)邏輯CTL~*與可能性互模擬[J];計(jì)算機(jī)科學(xué);2012年10期

，

本文編號(hào)：1840626