模糊转换系统的量化等价验证及模型检测研究

One of the main aims of formal verification method is to ensure the correctness of computerized systems. Traditional formal verification methods are two-valued or qualitative: a system satisfies, or not, a given specification while quantitative formal verification method can quantify to what extend a system meets its specification. Fuzzy formal verification methods which combine fuzzy logic theory with formal verification methods, have been formed gradually and are central in designing and analysis of fuzzy discrete event systems and other systems. .Equivalence verifications and temporal logic are two principal formal verification methods. This project will consider equivalence verifications and temporal logic in the framework of completed residuated lattice-valued logic to form a new type of fuzzy quantitative verification method. Based on completed residuated lattice-valued fuzzy transition systems, the main contents of this project are as follows: We first present the fuzzy language relation and fuzzy bisimulation relation, then introduce the temporal logic fuzzy CTL* as a specification language of fuzzy transition systems and discuss its model checking problem; Further, we relate these two fuzzy relations with fuzzy CTL* in terms of logical characterizations; Finally, the results obtained in this project are applied to the modeling and analysis of fuzzy discrete event systems. The research will lay a solid foundation for quantitative verification methods of fuzzy systems.

形式化验证方法是借助数学的方法来保证计算机系统的正确性。经典的形式化验证是一种定性的验证方法，其验证一个系统满足或不满足其规范，后来人们建立的量化形式化验证方法能分析出一个系统多大程度满足其规范。近年来，基于模糊逻辑发展量化形式化验证方法引起了学术界的关注，产生了模糊量化验证方法，在模糊离散事件系统的设计和分析等方面有着重要的应用。.等价验证和模型检测是两种常用的形式化验证方法。本项目从完备剩余格逻辑的角度去研究等价验证和模型检测，建立模糊量化验证理论。在基于完备剩余格的转换系统基础上，本项目主要研究以下内容：提出模糊语言关系和格值互模拟验证方法；引入模糊CTL*作为系统的规范语言，解决它的模型检测问题；用模糊CTL*建立模糊语言关系和模糊互模拟关系的逻辑刻画；将研究成果用于模糊离散事件系统的建模、分析和验证。本项目的研究将为模糊系统的量化验证提供理论基础和技术支撑。

近年来，基于模糊逻辑发展量化形式化验证方法引起了学术界的关注，产生了模糊量化验证方法，在模糊系统的设计和分析等方面有着重要的应用。鉴于等价验证和模型检测是两种常用的形式化验证方法，本项目基于完备剩余格逻辑的角度去研究等价验证和模型检验，主要取得了以下成果：（1）提出取值于完备剩余格的不确定型模糊自动机模型，引入两种不同区分能力的语言等价关系来分析不确定型模糊自动机的行为；（2）使用Gödel逻辑扩展交替迹包含和交替模拟这两种精化关系，证明了所得到的两种关系继承了各自相应的经典关系的基本性质；（3）研究了不确定型Kripke结构上的不确定型模糊计算树逻辑的模型检验问题，并说明该问题能在多项式时间内解决；（4）讨论了无限状态的模糊系统的可达性问题，为使用模型检验技术验证无限状态的模糊系统奠定了基础。本项目的研究成果可用于形式化描述、开发和验证模糊系统。