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

【摘要】：在實(shí)際生活中,較大的和復(fù)雜的系統(tǒng)在運(yùn)行過程中不可避免地出現(xiàn)不確定的、不一致的信息,所以經(jīng)典的模型檢測不能處理并發(fā)系統(tǒng)中所有的驗(yàn)證問題.為了處理概率不確定性的系統(tǒng)驗(yàn)證,Baier和Katoen介紹了基于概率測度的模型檢測的原理和方法,Hart和Sharir將概率論應(yīng)用于模型檢測.而現(xiàn)實(shí)生活中有很多復(fù)雜的問題不滿足概率測度下的可加性,這些問題并不能用概率模型進(jìn)行驗(yàn)證,因此對非可加性測度下模型檢測的研究具有理論與實(shí)際意義.可能性測度是一種非可加性測度,基于可能性測度的線性時(shí)序邏輯(LTL)和計(jì)算樹邏輯(CTL)模型檢測已經(jīng)有一些重要的研究成果,但還有一些重要且關(guān)鍵的問題尚未探討：可能性測度下瞬時(shí)測度是否存在,瞬時(shí)可能性測度與可達(dá)可能性測度的關(guān)系,計(jì)算樹邏輯和可能性測度下計(jì)算樹邏輯(PoCTL)的關(guān)系等,本文就針對這幾個問題進(jìn)行探討. 論文主要做了以下兩方面的工作： (1)提出了瞬時(shí)可能性測度的概念,并用構(gòu)造法證明了在轉(zhuǎn)移步數(shù)限制下的可達(dá)可能性測度與可達(dá)瞬時(shí)可能性測度相等,受限的轉(zhuǎn)移步數(shù)限制下的可達(dá)可能性測度與受限可達(dá)瞬時(shí)可能性測度相等.探討了在可能性測度下并、交、補(bǔ)運(yùn)算成立的條件以及那些LTL性質(zhì)成立,特別是在強(qiáng)連通子集下重復(fù)可達(dá)事件和持久性事件的性質(zhì). (2)基于可能性測度對CTL做了進(jìn)一步的探討,給出了PoCTL公式與CTL公式和PoCTL公式與PoCTL公式分別等價(jià)的定義.利用公式的等價(jià)性證明了PoJ(φ)在非運(yùn)算下成立.對PoCTL中事件的可能性大于0以及等于1時(shí)的性質(zhì)做了詳細(xì)的探討,深入研究了PoCTL與CTL的異同,得出了CTL公式是PoCTL公式的一個真子集.對CTL公式中的重復(fù)事件和持久性事件的定性性質(zhì)和定量性質(zhì)進(jìn)行了詳細(xì)的研究,通過例子說明了在可能性測度與概率測度下CTL公式的區(qū)別.最后給出了PoCTL模型檢測的步驟和時(shí)間復(fù)雜度,說明了模型檢測的可行性.
[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é)位級別】：碩士
【學(xué)位授予年份】：2013
【分類號】：TP306;O211

【參考文獻(xiàn)】

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

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

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

，

本文編號：1840626