Abstract: This paper establishes the intuitionistic fuzzy Kripke structure (IFKS) model, proposes the intuitionistic fuzzy measure theory based on IFKS, and expounds a series of properties of IFKS. Then, this paper proves that the intuitionistic fuzzy probability (IFP) of every path in an IFKS is the infimum of the IFP of the initial state and every translation in the path, and the IFP of those paths that start from the same initial state is the supremum of their IFP. This paper also defines the transfer matrix of path P and its transitive closureP⁺,, gives an algorithm which can be used for calculating P⁺, and analyzes the complexity of the algorithm. After that, this paper builds the intuitionistic fuzzy computation tree logic (IFPCTL) theory, and discusses the equivalence of a set of formula about IFPCTL, possibilistic computation tree logic (PoCTL) and computation tree logic (CTL). Finally, this paper gives a set of equivalent formula about IFPCTL and PoCTL, and a set of inequitable formula about IFPCTL and CTL at the same time.

Key words: intuitionistic fuzzy Kripke structure, intuitionistic fuzzy probability, intuitionistic fuzzy computation tree logic, model checking

摘要： 建立了直觉模糊Kripke结构（intuitionistic fuzzy Kripke structure，IFKS）模型，提出了基于直觉模糊Kripke结构的直觉模糊测度空间理论，阐述了IFKS的一系列性质。证明了任一路径转移的直觉模糊可达度（intuitionistic fuzzy probability，IFP）为初始状态的直觉模糊测度与各转移的IFP所取下确界，任一状态出发的所有路径上路径转移的IFP为所有路径可达度的上确界。给出了路径转移矩阵P及其传递闭包P⁺的概念，给出了通过计算路径转移矩阵传递闭包，计算路径可达度的算法，并分析了算法的复杂度。提出了直觉模糊计算树逻辑（intuitionistic fuzzy computation tree logic，IFPCTL）理论，讨论了一组IFPCTL、可能测度计算树逻辑（possibilistic computation tree logic，PoCTL）和经典计算树逻辑（computation tree logic，CTL）公式的等价性。最后给出了一组等价的IFPCTL和PoCTL公式以及一组不等价的IFPCTL和CTL公式。

关键词: 直觉模糊Kripke结构, 直觉模糊测度, 直觉模糊计算树逻辑, 模型检测