Characteristic Formulae (continued)

In a previous post, I briefly discussed the notion of characteristic formula for a state in a labelled transition system using Hennessy-Milner logic (HML) as the underlying property specification language. In light of its beautiful connection with bisimilarity, HML and its variations are prime candidates for logics in which to express characteristic properties for bisimulation-like relations. However, there are other options.

A classic result on characteristic formulae was obtained in the paper

Browne, M. C.; Clarke, E. M.; Grümberg, O. Characterizing finite Kripke structures in propositional temporal logic. Theoret. Comput. Sci. 59 (1988), no. 1-2, pp. 115-131.

The above paper shows that for any finite Kripke structure, i.e., a labelled transition graph with an initial state, it is possible to construct a Computation Tree Logic formula uniquely characterizing that finite Kripke structure. Browne, Clarke and Grümberg call the notion of equivalence matching "logical equivalence wrt CTL" E-equivalence. Two states are said to be E-equivalent if they have the same labelling of atomic propositions, and transitions to other states preserve the E-equivalence. (Surprise, surprise! This is just bisimilarity for Kripke structures.) It turns out that, modulo E-equivalence, finite Kripke structures are characterized by CTL formulae containing the "next-time" operator. (A formula of the form X φ, read "next φ", states that φ has to hold at the next state of the computation path.)

Another characteristic formula result is presented in that paper for an equivalence between states called S-equivalence (equivalence with respect to stuttering) . Two state sequences are said to correspond if each can be partitioned into finite blocks of identically labelled states such that each state of the ith block in one sequence is E-equivalent to each state in the ith block of the other sequence. Two states are said to be S-equivalent if, for each state sequence starting at one, there is a corresponding state sequence that starts at the other.

Theorem: S-equivalence classes of states in a finite Kripke structure are completely characterized by next-time-free CTL formulae.

The absence of the next-time operator is expected in light of the inability of S-equivalence to "count" the number of steps in a stuttering sequence. S-equivalence is closely related to van Glabbeek's and Weijland's branching bisimilarity. Logical characterizations of branching bisimilarity have been offered by De Nicola and Vaandrager in the paper:

R. De Nicola and F.W. Vaandrager. Three logics for branching bisimulation. Journal of the ACM, 42(2):458-487, 1995.

Kucera and Schnoebelen have presented a refinement of the above classic theorem by Browne, Clarke and Grümberg in the paper

A. Kucera and Ph. Schnoebelen. A general approach to comparing infinite-state systems with their finite-state specifications. Theor. Comput. Sci. 358(2-3): 315-333 (2006).

In a follow-up post, I'll try to wind up this brief three-part discussion of characteristic formulae by mentioning a couple of results on characteristic formulae for timed automata.