摘要
模型检测作为一种形式化验证技术,已被广泛应用于各种并发系统的正确性验证。针对具有非确定性选择和广义可能性分布的并发系统,引入广义可能性决策过程作为此类系统的模型;给出描述其性质的规范语言广义可能性计算树逻辑的概念;研究此类系统的广义可能性计算树逻辑模型检测问题。结论表明,其模型检测算法的时间复杂度也为多项式时间。所获得的结果扩大了广义可能性测度在模型检测中的应用范围。
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.
出处
《计算机工程与科学》
CSCD
北大核心
2015年第11期2162-2168,共7页
Computer Engineering & Science
基金
国家自然科学基金资助项目(11271237
61228305
61462001)
北方民族大学资助项目(2014XB213)
关键词
并发系统
广义可能性决策过程
广义可能性计算树逻辑
模型检测
concurrent systems
generalized possibilistic decision process
generalized possibilistic computation tree logic （GPCTL）
model checking
