Characterizing finite Kripke structures in propositional temporal logic (Q1123183)

A (finite) Kripke structure is a triple \(M=<S,R,{\mathcal L}>\), where S is the (finite) set of states, \(R\subseteq S\times S\) is a (total) transition relation and \({\mathcal L}\) is a valuation from states to the set of subsets of atomic formulas of a given (propositional) temporal logic theory \({\mathcal T}\). The chosen logics are \(CTL^*\) [\textit{E. A. Emerson} and \textit{J. Y. Halpern}, J. Assoc. Comput. Mach. 33, 151-178 (1986; Zbl 0629.68020)] and CTL. CTL is a restricted subset of \(CTL^*\) that permits only branching time operators (linear time operator being disallowed) such that each path quantifier must be immediately followed by exactly one of the operators G (``always''), F (``sometimes''), X (``next time'') or U (``until''). It is shown that if two finite Kripke structures can be distinguished (via valid formulas) in \(CTL^*\), then they can also be distinguished in CTL. The formulas implied characterize the Kripke structures via a natural equivalence relation (similar to bisimulation), or via a ``stuttering'' relation (by eliminating the ``next time'' operator). A polynomial time algorithm for computing the equivalence relation via stuttering is also given.