广义可能性决策过程的计算树逻辑模型检测

模型检测作为一种形式化验证技术,已被广泛应用于各种并发系统的正确性验证。针对具有非确定性选择和广义可能性分布的并发系统,引入广义可能性决策过程作为此类系统的模型;给出描述其性质的规范语言广义可能性计算树逻辑的概念;研究此类系统的广义可能性计算树逻辑模型检测问题。结论表明,其模型检测算法的时间复杂度也为多项式时间。所获得的结果扩大了广义可能性测度在模型检测中的应用范围。

Computation tree logic model checking for generalized possibilistic decision processes

Model checking is a widespread formal technique for verifying the correctness of concurrent systems. We introduce the generalized possibilistic decision process as the model of the systems, which have non deterministic choices and generalized possibility distributions.To describe its attributes, we define the concept of generalized possibilistic computation tree logic (GPCTL) specification language and study the GPCTL model checking problems.The time complexity of the computation tree logic model checking algorithm shows to be polynomial time. The results obtained in this paper extend the application scope of model checking based on generalized possibility measurement.