【作者】 李丽君；

【导师】 李永明；

【作者基本信息】 陕西师范大学 ， 计算机软件与理论， 2012， 硕士

【摘要】 模型检测是一种很重要的自动验证技术.1981年,由Clarke和Emerson以及Quielle和Sifakis最早提出,它主要通过状态搜索或不动点计算来验证有穷状态并发系统的命题性质.它可以自动执行,并能在系统不满足性质时提供反例.在很多情况下,可以把模型检测和各种归纳原则结合起来验证非有穷状态系统.在经典的模型检测中,Kripke结构是很重要的一种研究模型,线性时序逻辑(LTL)是一种研究线性性质的重要时序逻辑工具.将二者联系起来研究系统满足线性时间性质是非常有必要的.2008年,Baier和Katoen详细研究了基于概率测度下以马尔科夫链为概率系统模型的模型检测方法和相关应用.另一方面,自Zadeh在1965年提出模糊集的理论以来,许多学者致力于模糊集理论及应用方面的研究工作.模糊测度作为模糊集理论的一个分支是经典测度的延拓,它重点研究一种非可加情况,而大多数复杂的实际问题都是非可加的情况.因此有必要研究具有非可加测度的非确定系统的模型检测的理论及应用问题.本文针对一种常见的非可加测度：可能性测度,研究基于可能性测度情形下的模型检测理论.具体来说,我们主要针对可能性测度下的线性性质的模型检测进行研究.论文的主要工作表现在以下方面：1.定义了可能的Kripke结构,分析了可能的Kripke结构在可能性测度下的线性时间属性(LTL)模型检测.并对可能性测度和概率测度的一些性质进行了比较.2.首先给出了有穷的可能的Kripke结构满足可达性、受限可达性的可能性测度的代数表达形式及相应的计算方法,并与马尔科夫链满足线性性质的概率测度进行了比较.其次通过使用有穷自动机将可能的Kripke结构满足可达性等性质推广到了满足正则安全性、ω-正则性等一般的线性时间(LT)性质.进而得出结论：在可能的Kripke结构上的正则安全性、ω-正则性的验证可以转化为乘积可能Kripke结构(可能的Kripke结构和非确定型有穷自动机的乘积)上的可达性和重复可达性的验证问题,并对该方法的应用进行了实例分析.最后对本文的基本内容作了总结,提出将来可以研究的问题.更多还原

【Abstract】 Model checking is a very important approach of automatic verification. It was put forward by Clarke, Emerson, Quielle and Sifakis in1981. Using model checking method, we can verify the proposition of the concurrent systems with the finite state mainly through the state search. Model checking method can execute automatically, and provide counterexample when the system can’t fulfil the property. In many situations, we can verify infinite state system by the combination of model checking and other kinds of inductive principles.In classical model checking, Kripke structure is an important model and linear temporal logic is an important sequential logic tool in studying linear property. In2008, Baier and Katoen systematically introduced the principle and method of model checking based on probability measure and related applications with Markov chain model for probability system. On the other hand, since Zadeh proposed the theory of fuzzy sets in1965, many scholars have been devoting themselves to the research in this theory and its application. As a branch of the theory of fuzzy sets, possibility measure is a development of classical measure, which focuses on non-additive cases that is different from the probability measure. Most problems in real situations are complicated and non-additive; therefore, it is necessary to do some research work in the theory and application of model-check on non-deterministic systems of non-additive measure. And this paper attempts to initiate an LTL model-check based on possibility measure.This paper we discuss a common not-additive measure:probability measure and study the theory of model checking based on the possibility measure. Specifically, we mainly study model checking of linear property under the probability measure. This forms the main topic of this paper.1. We define possibilistic Kripke structure and analyse the Linear Temporal Logic (LTL) model checking in possibilistic Kripke structure using possibility measure. Then we compare the propety of possibility measure and probability measure.2. Firstly, we study the algebraic expressions and the calculation method of possibility measure which finite possibilistic Kripke structure satisfy reachability and repeated reachability linear-time properties and compare with probability measuret of the Markov chain model satisfy the two properties. Secondly, we introduce standard safety property and co-regular property in possibilistic Kripke structur and thoroughly study the verification of regular safety property and ω--regular property using finite automata. Then we get the conclusion:the verification of regular safety property and ω-regular property in finite possibilistic Kripke structure can be transformed into the verification of reachability property and repeated reachability property in the product possibilistic Kripke structure introduced in this paper and we give several examples to illustrate the methods presented. Finally, we summarise the basic contents of this paper and propose some problems about future research.更多还原