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

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