Temporal Logics

Temporal Logics
Kripke structures: Kripke structures are finite-state machines used to model concurrent systems. A Kripke structure is a four-tuple S, s0,R, L where S is a finite set of states, s0 is an initial state, R ⊆ S × S is a total relation known as the reachability relation, and L : S → 2P is a labeling function, with P being a set of atomic propositions. It is standard practice to require that R be total, as Kripke structure are used to model infinite computations (in modeling finite computations, terminal states are equipped with transitions to themselves, thus in effect making R total).
The fact that we choose one initial state is a matter of convenience. Figure 22.1 (bottom) presents two Kripke structures. In the Kripke structure on the left, S = {s0, s1, s2}, s0 = s0, R is shown by the directed edges, and L by the subsets of {a, b} that label the states. In its behavior over time, this Kripke structure asserts a and b true in

the first time step, b true in the second time step, and a in the third time step. In the fourth time step, it may assert either a or b. One of these sequences is shown in the middle – namely, choosing to assert a in the fourth time step, and b in the fifth. When a label is omitted (e.g., there is no b in state s2), we are effectively asserting ¬b. Therefore, the assertion in state s3 is ¬a∧¬b. The corresponding “waveforms2” (as if viewed on an oscilloscope) are shown at the top of this figure.
From these discussions it is clear that we model the behavior of systems in terms of the truth values of a set of Boolean variables. This is the most common approach taken when modeling systems as finitestate machines.We therefore let P be the set of these Boolean variables. There are of course other ways to model systems. For instance, if one were to employ a set of Boolean variables B and a set of integer variables I to model a system, P would consist of B as well as propositions over integers, such as i > 2 or i = j 1. In any case, knowing the truth of the atomic propositions P, it is possible to calculate the truth of any Boolean proposition built over P.
Each state s ∈ S is an equivalence class of time points, while R models how time advances. Whenever the system is at a state s ∈ S, a fixed set of Boolean propositions determined by L are true. Since S is finite, we can immediately see that the temporal behavior of systems modeled using Kripke structures recur over time, thus basically generating a regular language of truth values of the propositions in P. For example, Figure 22.1 shows how the truth of the Boolean proposition a ∨ b varies with time. Since either a or b is always true, a ∨ b is always true for the Kripke structure on the left; that is not the case for the Kripke structure on the right, as we can enter state s3 where both a and b are false.