基于可能性测度的时序逻辑性质研究

发布时间：2018-05-03 23:37

本文选题：可能的Kripke结构 + 可能性测度　；参考：《陕西师范大学》2013年硕士论文

【摘要】：在实际生活中,较大的和复杂的系统在运行过程中不可避免地出现不确定的、不一致的信息,所以经典的模型检测不能处理并发系统中所有的验证问题.为了处理概率不确定性的系统验证,Baier和Katoen介绍了基于概率测度的模型检测的原理和方法,Hart和Sharir将概率论应用于模型检测.而现实生活中有很多复杂的问题不满足概率测度下的可加性,这些问题并不能用概率模型进行验证,因此对非可加性测度下模型检测的研究具有理论与实际意义.可能性测度是一种非可加性测度,基于可能性测度的线性时序逻辑(LTL)和计算树逻辑(CTL)模型检测已经有一些重要的研究成果,但还有一些重要且关键的问题尚未探讨：可能性测度下瞬时测度是否存在,瞬时可能性测度与可达可能性测度的关系,计算树逻辑和可能性测度下计算树逻辑(PoCTL)的关系等,本文就针对这几个问题进行探讨. 论文主要做了以下两方面的工作： (1)提出了瞬时可能性测度的概念,并用构造法证明了在转移步数限制下的可达可能性测度与可达瞬时可能性测度相等,受限的转移步数限制下的可达可能性测度与受限可达瞬时可能性测度相等.探讨了在可能性测度下并、交、补运算成立的条件以及那些LTL性质成立,特别是在强连通子集下重复可达事件和持久性事件的性质. (2)基于可能性测度对CTL做了进一步的探讨,给出了PoCTL公式与CTL公式和PoCTL公式与PoCTL公式分别等价的定义.利用公式的等价性证明了PoJ(φ)在非运算下成立.对PoCTL中事件的可能性大于0以及等于1时的性质做了详细的探讨,深入研究了PoCTL与CTL的异同,得出了CTL公式是PoCTL公式的一个真子集.对CTL公式中的重复事件和持久性事件的定性性质和定量性质进行了详细的研究,通过例子说明了在可能性测度与概率测度下CTL公式的区别.最后给出了PoCTL模型检测的步骤和时间复杂度,说明了模型检测的可行性.
[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.
【学位授予单位】：陕西师范大学
【学位级别】：硕士
【学位授予年份】：2013
【分类号】：TP306;O211

【参考文献】