模型检测作为一种自动的形式化验证方法，在计算机软硬件系统验证方面越来越受到学术界和工业界的关注。经典模型检测只强调系统满足功能需求性质的绝对正确，为了分析具有量化行为特征的系统满足其功能需求和性能指标等非功能需求，学者们提出了定量模型检测方法。本项目将模型检测方法、广义可能性测度理论和决策过程理论结合起来，研究基于决策过程的广义可能性时序逻辑的符号模型检测方法。在广义可能性决策过程模型基础上，引入广义可能性时序逻辑描述系统的定量属性，分析可能性时序逻辑的性质和表达能力，讨论互模拟等价及其逻辑刻画。通过引入广义可能性线性时间属性，研究可达性、正则安全属性，活性等属性的符号模型检测问题。最后给出广义可能性时序逻辑的符号模型检测算法，编写模型检测工具并应用于交通信息物理融合系统的验证。本项目的研究拓展了模型检测的应用范围，也为最优化问题的求解提供了新的理论和方法。

As a kind of formal automatic verification method, model checking has been paid more and more attention by academia and industry for the verification of computer software and hardware system. The classical model checking method is qualitative, with the emphasis put on the absolute correctness of system satisfying the specifications. In order to verify the specification of systems are endowed with quantitative behavior characteristics and hence need to be analyzed quantitatively as to what extent they meet the system’s functional and nonfunctional requirements, scholars put forward quantitative model checking method. This project is an extension of the quantitative model checking method. A symbolic model checking method of generalized possibility temporal logic based on decision process is studied by combining the decision processes theory, generalized possibility measure and model checking method. We intend to:.1. Based on the generalized possibilistic decision process model, the generalized possibilistic temporal logic will be introduced to describe the specification of fuzzy systems and analyze the probability temporal logic and their expressive power. We provide related concepts of bisimulation equivalence, and give its logical characterization..2. By introducing generalized possibilistic linear time properties, symbolic model checking of reachability, such as eventually reachability, always reachability, persistent reachability and repeated reachability，is studied. And we study the symbolic model checking problems for generalized possibilistic regular safety properties and generalized possibilistic omega-regular properties..3. We give respective symbolic model checking algorithms for generalized possibilistic CTL、generalized possibilistic LTL and generalized possibilistic CTL*, and develop a model checking tool that can be applied to the modeling and verification of Transformation Cyber-Physical System. .The project extends the application range of the fuzzy model checking method, and provides a new method for solving the optimization problems.