Model checking fuzzy computation tree logic

Traditional temporal logics such as linear temporal logic and computation tree logic are widely used to specify properties of reactive systems. Model checking is a well-established technique for verifying if a desired property described as a temporal logic formula holds over a reactive system model. This paper presents fuzzy computation tree logic (FCTL), a fuzzy extension of temporal logics, by combining general fuzzy logic with computation tree logic, and discusses its model checking problem. First, the notion of fuzzy Kripke structures (FKSs) and the syntax and semantics of their specification language FCTL are introduced. Then we give a direct model checking algorithm for FCTL over FKS. On the other hand, we study when FCTL model checking problem can be reduced to classical model checking ones, and give a reduction method for an important fragment of FCTL.