SKEDSOFT

Automata | Comp. Sc. Engg.

Temporal formulas are Kripke structure classifiers!: CTL formulas can be viewed as classifiers of Kripke structures or as classifiers of computation trees. Both these views are equivalent (knowing the Kripke structure, we can obtain the computation tree, and vice versa). LTL formulas can also be viewed in the same manner. We now explain these ideas, beginning with CTL first.

CTL formulas are Kripke structure classifiers: Given a CTL formula ϕ, all possible computation trees fall into two bins—models and non-models.5 The computation trees in the model (‘good’) bin are those that satisfy ϕ while those in the non-model (‘bad’) bin obviously falsify ϕ. Consider the CTL formula AG (EF (EG a)) as an example. Here,

  • ‘A’ is a path quantifier and stands for all paths at a state
  • ‘G’ is a state quantifier and stands for everywhere along the path
  • ‘E’ is a path quantifier and stands for exists a path
  • ‘F’ is a state quantifier and stands for find (or future) along a path
  • ‘X’ is a state quantifier and stands for next along a path

The truth of the formula AG (EF (EG a)) can be calculated as follows:

  • In all paths, everywhere along those paths, EF (EG a) is true
  • The truth of EF (EG a) can be calculated as follows:
  • − There exists a path where we will find that EG a is true.
  • − The truth of EG a can be calculated as follows:

∗ There exists a path where a is globally true.

In CTL, one is required to use path quantifiers (A and E) and state quantifiers (G, F, X, and U) in combinations such as AG, AF, AX, AU, EG, EF, EX, and EU. In other temporal logics such as CTL*, these operators may be used separately. Coming back to the examples in Figure 22.1, AG (EF (EG a)) — which means, Starting from any state s of the system (s0, s1, or s2 in our case), one can find a future reachable state t such that starting from t, there is an infinite sequence of states along which a is true is true of the Kripke structure on the left, but not the one on the right.
This is because wherever we are in the “machine” on the left, we can be permanently stuck in state s2 that emits a. In the machine on the right, a can never be permanent. As another example, with respect to the Kripke structures of Figure 22.2, the assertion AG(b ⇒ EX c) (“wherever we are in the computation, if b is true now, that means that there exists at least one next state where c is true”) is true of the bottom Kripke structure but not the top Kripke structure.
 

LTL formulas are Kripke structure classifiers
Turning back to LTL, at its core it is a logic of infinite computations or truth-value sequences (“waveforms”). For example, the LTL formula (a ∨ b) (also written as G (a ∨ b) or “henceforth a ∨ b”) is true with respect to the computation (waveform) shown on the left-hand side of Figure 22.1 against (a ∨ b) = 1, while it is false with respect to the waveform shown on the right.
It is customary to view LTL also as a Kripke structure (or computation tree) classifier. This is really a simple extension of the basic idea behind LTL. Under this view, an LTL formula ϕ is true of a computation tree if and only if it is true of every infinite path in the tree. As an example, no LTL formula can distinguish the two Kripke structures given in Figure 22.2, as they both have the same set of infinite paths.