Temporal Logic

A finite state system can be described as a tuple:

$$\mathcal{M} = <\mathcal{S},\mathcal{I},\mathcal{R}, \mathcal{L}>$$

where $\mathcal{S}$ is a finite set of states, $\mathcal{I} \subseteq \mathcal{S}$ is the set of initial states, and $\mathcal{R} \subseteq \mathcal{S}\times \mathcal{S}$ is the transition relation, specifying the possible transitions from state to state. $\mathcal{L}$ is a function that labels states with the atomic propositions from a given language. Such a tuple is called state transition graph or Kripke structure [44].

  

Figure 1: A State Transition Graph and its unwinding.

Temporal logics are used to predicate over the behavior defined by Kripke structures. A behavior in a Kripke structure is obtained starting from a state $s \in \mathcal{I}$, and then repeatedly appending states reachable through $\mathcal{R}$. We require that the transition relation $\mathcal{R}$ be total.² As a consequence all the behaviors of the system are infinite. Since a state can have more than one successor, the structure can be thought of as unwinding into an infinite tree, representing all the possible executions of the system starting from the initial states. Figure 1 shows a state transition graph and its unwinding from the state labeled with ``A''.

Two useful temporal logics are Computation Tree Logic (called CTL) and Linear Temporal Logic (called LTL). They differ in how they handle branching in the underlying computation tree. In CTL temporal operators it is possible to quantify over the paths departing from a given state. In LTL operators are intended to describe properties of all possible computation paths.

The syntax of CTL formulas is given by the following rules:

1.

any atomic proposition is a CTL formula;

2.

if $\alpha$ and $\beta$ are CTL formulas, then $\alpha \bullet \beta$ and $\neg \alpha$ are CTL formulas, where $\bullet$ is any boolean connective ( $\wedge, \vee, \ldots{}$);

3.

if $\alpha$ and $\beta$ are CTL formulas, then $\mathbf{EX} \alpha$, $\mathbf{EG} \alpha$, $\mathbf{E}[\alpha \mathbf{U} \beta]$ are CTL formulas.

Figure 2 describes the intuitive meaning of CTL formulas. $\mathbf{EX} \alpha$ means that there exists ( E) a path starting from a state $s_0 \in \mathcal{S}$ in which in the next ( X) state $\alpha$ holds. $\mathbf{EG} \alpha$ means that there exists a path starting from a state s₀ in which globally ( G) $\alpha$ holds. $\mathbf{E}[\alpha \mathbf{U} \beta]$ there exists a path starting from a state s₀ in which $\alpha$ holds until ( U) $\beta$ holds. The other CTL operators (e.g., $\mathbf{AF} \alpha$, meaning for all paths eventually $\alpha$) can be derived from these three according to the rules listed in Table 1.

 

Table 1: Definition of CTL operators.

$\mathbf{AX} \alpha = \neg \mathbf{EX}(\neg \alpha)$	For all paths, in the next state $\alpha$
$\mathbf{EF} \alpha = \mathbf{E}[ \top \mathbf{U} \alpha]$	There exists a path in which eventually $\alpha$
$\mathbf{AG} \alpha = \neg \mathbf{EF}(\neg \alpha)$	Invariantly $\alpha$
$\mathbf{A}[\alpha \mathbf{U} \beta] = \neg \mathbf{E}[\neg \beta \mathbf{U} \neg \alpha \wedge \neg \beta] \wedge \neg \mathbf{EG} \neg \beta$	For all paths, $\alpha$ until $\beta$
$\mathbf{AF} \alpha = \mathbf{A}[\top \mathbf{U} \alpha]$	For all paths, eventually $\alpha$

 

  

Figure 2: The meaning of temporal modalities.

The syntax of LTL formulas is the following:

1.

any atomic proposition is an LTL formula;

2.

if $\alpha$ and $\beta$ are LTL formulas, then $\alpha \bullet \beta$ and $\neg \alpha$ are LTL formulas, where $\bullet$ is any boolean connective ( $\wedge, \vee, \ldots{}$);

3.

if $\alpha$ and $\beta$ are LTL formulas, then $\mathbf{X} \alpha$, $\mathbf{G} \alpha$, $[\alpha \mathbf{U} \beta]$ are LTL formulas.

The model checking problem can be formally formulated as follows. Given a Kripke structure $\mathcal{M}$ and a temporal logic formula $\varphi$, find the set of all states that satisfy $\varphi$, namely the set of states

$$\{s \in \mathcal{S}\; \vert\; \mathcal{M},s \models \varphi \}$$ (1)

We say that the system satisfies the specification provided that all the initial states are in the set $\{s \in \mathcal{S}\; \vert\; \mathcal{M},s \models \varphi \}$:

$$\mathcal{I} \subseteq \{s \in \mathcal{S}\; \vert\; \mathcal{M},s \models \varphi \}$$ (2)

Each CTL formula $\varphi$ is identified by the set of states where it holds, $\{s \in \mathcal{S} \vert \mathcal{M},s \models \varphi\}$. CTL operators may be characterized as a least or a greatest fixpoint of an appropriate predicate transformer [12]:

• $\mathbf{EG}\alpha = \mathbf{gfp}_Z [ \alpha \wedge \mathbf{EX} Z ]$
• $\mathbf{E}[ \alpha \mathbf{U} \beta] = \mathbf{lfp}_Z [\beta \vee (\alpha \wedge \mathbf{EX} Z)]$

This suggests an algorithm for symbolic model checking which is driven by the structure of the formula. For example, the computation of $\mathbf{E}[ \alpha \mathbf{U} \beta] = \mathbf{lfp}_Z [\beta \vee (\alpha \wedge \mathbf{EX} Z)]$ corresponds to the following iterations:

$$\begin{array}{l} s_0 = \bot\\ s_1 = \beta \vee (\alpha \we... ...a \wedge \mathbf{EX} \beta))}^{s_2})\\ \ldots{} \end{array}$$

Iterations continue until s_i+1 = s_i. The existence of least and greatest fixpoints is guaranteed by the monotonicity of the predicate transformers and by the finiteness of the domain [12].