CHARACTERIZING FINITE KRIPKE STRUCTURES IN PROPOSITIONAL TEMPORAL LOGIC

We show that if two finite Kripke structures can be distinguished by some CTL formula that contains both branching-time and linear-time operators, then the structures can be distinguished by a CTL formula that contains only branching-time operators. Our proof involves showing that, for any finite Kripke structure M, it is possible to construct a CTL formula FM that uniquely characterizes M. Our first construction of FM requires the use of the nexttime operator. We also consider the case in which the nexttime operator is disallowed in CTL formulas. The proof, in this case, requires another notion of equivalence - equivalence with respect to stuttering. We also give a polynomial algorithm for determining if two structures are stuttering equivalent and discuss the relevance of our results for temporal logic model checking and synthesis procedures.