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

【Abstract】 Partial state spaces model checking is a new technique to solve problem of state explosion, whose partial state spaces are represented by partial Kripke structures. This paper mainly discusses the problem of model checking CTL formula with fairness constrained by partial state spaces technique. This paper defines a partial fair Kripke structure, and a fair preorder to represent the partial state spaces and their preorder. In addition, a 3-valued fair CTL(Computation-Tree Logic)semantics and a pertinent theorem are also given.更多还原