具有公平性约束的CTL部分状态空间模型检测

摘要：

检测部分状态空间是近年来出现的有效解决状态爆炸的模型检测技术,部分Kripke结构是描述部分状态空间的形式框架.文章主要讨论一类具有公平性约束条件的CTL(计算树逻辑)模型检测问题.定义了部分公平Kripke结构和公平序,分别来表征部分公平状态空间和它们之间的序关系.并给出相应的3值CTL语意和相关定理来说明部分状态空间模型检测技术同样适用于具有公平性约束条件的CTL模型检测问题.

关键词：公平性、部分Kripke结构、计算树逻辑、模型检测

所属期刊栏目：29

分类号：TP274+.5(自动化技术及设备)

资助基金：国家自然科学基金60173103

在线出版日期：2004-01-08（万方平台首次上网日期，不代表论文的发表时间）

页数：共3页

页码：10-12