Temporal Logic: Formulas, Models, Tableaux

Abstract

Temporal logic is a formal system for reasoning about time. Temporal logic has found extensive application in computer science, because the behavior of both hardware and software is a function of time. This section will follow the same approach that we used for other logics: we define the syntax of formulas and their interpretations and then describe the construction of semantic tableaux for deciding satisfiability.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Temporal logic is a formal system for reasoning about time. Temporal logic has found extensive application in computer science, because the behavior of both hardware and software is a function of time. This section will follow the same approach that we used for other logics: we define the syntax of formulas and their interpretations and then describe the construction of semantic tableaux for deciding satisfiability.

Unlike propositional and first-order logics whose variants have little theoretical or practical significance, there are many temporal logics that are quite different from each other. A survey of this flexibility is presented in Sect. 13.3, but you can skim it and go directly to Sect. 13.4 that presents the logic we focus on: linear temporal logic.

13.1 Introduction

Example 13.1

Here are some examples of specifications that use temporal concepts (italicized):

• After the reset-line of a flip-flop is asserted, the zero-line is asserted. The output lines maintain their values until the set-line is asserted; then they are complemented.

• If a request is made to print a file, eventually the file will be printed.

• The operating system will never deadlock.

The temporal aspects of these specification can be expressed in first-order logic using quantified variables for points in time:

$$ \begin{array}{l} \forall t_{1}(reset(t_1) \mathbin {\rightarrow }\exists t_{2}(t_{2}\geq t_{1} \,\wedge \, \mathit{zero}(t_{2}))),\\ \\ \forall t_{1}\exists n(output(t_1) = n \,\wedge\\ \hspace*{2em} \exists t_{2}(t_{2}\geq t_{1} \,\wedge \, set(t_2) \,\wedge\, output(t_{2}+1) = 1-n \,\wedge\\ \hspace*{4em} \forall t_3(t_1 \leq t_3 < t_2 \,\mathbin {\rightarrow }\, output(t_3) = n))),\\ \\ \forall t_{1} (\mathit{RequestPrint}(t_{1}) \mathbin {\rightarrow }\exists t_{2}(t_{2}\geq t_{1} \,\wedge \, \mathit{PrintedAt}(t_{2}))),\\ \\ \forall t \neg \,\mathit{deadlocked}(t). \end{array} $$

 ■

The use of explicit variables for points of time is awkward, especially since the specifications do not actually refer to concrete values of time. ‘Eventually’ simply means at any later time; the specification does not require that the file be printed within one minute or ten minutes. Temporal logic introduces new operators that enable abstract temporal relations like ‘eventually’ to be expressed directly within the logic.

Temporal logics are related to formal systems called modal logics. Modal logics express the distinction between what is necessarily true and what is possibly true. For example, the statement ‘7 is a prime number’ is necessarily true because—given the definitions of the concepts in the statement—the statement is true always and everywhere. In contrast, the statement the head of state of this country is a king is possibly true, because its truth changes from place to place and from time to time. Temporal logic and modal logic are related because ‘always’ is similar to ‘necessarily’ and ‘eventually’ to ‘possibly’.

Although temporal and modal logics first appeared in Greek philosophy, their vague concepts proved difficult to formalize and an acceptable formal semantics for modal logic was first given by Saul Kripke in 1959. In 1977, Amir Pnueli showed that temporal logic can specify properties of concurrent programs and that Kripke’s semantics could be adapted to develop a formal theory of the temporal logic of programs. In this chapter and the next one we present the theory of linear temporal logic. Chapter 16 shows how the logic can be used for the specification of correctness properties of concurrent programs and for the verification of these properties. In that chapter, we will describe another temporal logic called computational tree logic that is also widely used in computer science.

13.2 Syntax and Semantics

13.2.1 Syntax

The initial presentation of the syntax and semantics of temporal logic will follow that used for general modal logics. We do this so that the presentation will be useful for readers who have a broader interest in modal logic and so that temporal logic can be seen within this wider context. Later, we specialize the presentation to a specific temporal logic that is used for the specification and verification of programs.

Definition 13.2

The syntax of propositional temporal logic (PTL) is defined like the syntax of propositional logic (Definition 2.1), except for the addition of two additional unary operators:

• □, read always,

• ◊, read eventually. ■

The discussion of syntax in Sect. 2.1 is extended appropriately: formulas of PTL are trees so they are unambiguous and various conventions are used to write the formulas as linear text. In particular, the two unary temporal logic operators have the same precedence as negation.

Example 13.3

The following are syntactically correct formulas in PTL:

$$p \wedge q,\quad \Box p,\quad \Diamond(p\wedge q) \mathbin {\rightarrow }\Diamond p,\quad \Box\Box p \mathbin {\leftrightarrow }\Box p,\quad \Diamond\Box p \mathbin {\leftrightarrow }\Box\Diamond p,\quad \neg \,\Diamond p \wedge \Box \neg \,q. $$

The formula $\neg \,\Diamond p \:\wedge\:\Box \neg \,q$ is not ambiguous because the temporal operators and negation have higher precedence than the conjunction operator. The formula can be written (¬ ◊p)∧(□¬ q) to distinguish it from ¬ (◊p∧□¬ q). ■

13.2.2 Semantics

Informally, □ is a universal operator meaning ‘for any time t in the future’, while ◊ is an existential operator meaning ‘for some time t in the future’. Two of the formulas from Example 13.1 can be written as follows in PTL:

$$ \Box(reset \mathbin {\rightarrow }\Diamond zero),\qquad \Box \neg \,\mathit{deadlocked}. $$

Interpretations of PTL formulas are based upon state transition diagrams. The intuitive meaning is that each state represents a world and a formula can have different truth values in different worlds. The transitions represent changes from one world to another.

Definition 13.4

A state transition diagram is a directed graph. The nodes are states and the edges are transitions. Each state is labeled with a set of propositional literals such that clashing literals do not appear in any state. ■

Example 13.5

Figure 13.1 shows a state transition diagram where states are circles labeled with literals and transitions are arrows. ■

Fig. 13.1

State transition diagram

In modal logic, necessarily means in all (reachable) worlds, whereas possibly means in some (reachable) world. If a formula is possibly true, it can be true in some worlds and false in another.

Example 13.6

Consider the formula A= the head of state of this country is a king. The formula is possibly true but not necessarily true. If the possible worlds are the different countries, then at the present time A is true in Spain, false in Denmark (because the head of state is a queen) and false in France (which does not have a royal house). Even in a single country, the truth of A can change over time if a king is succeeded by a queen or if a monarchy becomes a republic. ■

Temporal logic is similar to modal logic except that the states are considered to specify what is true at a particular point of time and the transitions define the passage of time.

Example 13.7

Consider the formula A= it is raining in London today. On the day that this is being written, A is false. Let us consider each day as a state and the transitions to be the passage of time from one day to the next. Even in London □A (meaning every day, it rains in London) is not true, but ◊A (meaning eventually, London will have a rainy day) is certainly true. ■

We are now ready to define the semantics of PTL. An interpretation is a state transition diagram and the truth value of a formula is computed using the assignments to atomic propositions in each state and their usual meaning of the propositional operators. A formula that contains a temporal operator is interpreted using the transitions between the states.

Definition 13.8

An interpretation $I$ for a formula A in PTL is a pair $(S,\rho )$, where $S = \{ s_1 , \ldots ,s_n \}$ is a set of states each of which is an assignment of truth values to the atomic propositions in A, $s_i :P \to \{ T,F\}$, and ρ is a binary relation on the states, ρ⊆S×S. ■

When displaying an interpretation graphically, the states are usually labeled only with the atomic propositions that are assigned T (Fig. 13.2). If an atom is not shown in the label of a state, it is assumed to be assigned F. Since it is clear how to transform one representation to the other, we will use whichever one is convenient.

Fig. 13.2

Alternate representation of the state transition diagram in Fig. 13.1

A binary relation can be considered to be a mapping from a state to a set of states ρ:S→2^S, so the relational notation (s ₁,s ₂)∈ρ will usually be written functionally as s ₂∈ρ(s ₁).

Example 13.9

In Fig. 13.2:

$$ \begin{array}{l@{\qquad}l} s_0(p)=T, & s_0(q)=F, \\[2pt] s_1(p)=T, & s_1(q)=T, \\[2pt] s_2(p)=F, & s_2(q)=T, \\[2pt] s_3(p)=F, & s_3(q)=F. \end{array} $$

$$ \begin{array}{l} \rho(s_0) = \{s_1, s_2\},\\[2pt] \rho(s_1) = \{s_1, s_2, s_3\},\\[2pt] \rho(s_2) = \{s_1\},\\[2pt] \rho(s_3) = \{s_2, s_3\}. \end{array} $$

 ■

Definition 13.10

Let A be a formula in PTL. $\upsilon _{I,s} (A)$, the truth value of A in s, is defined by structural induction as follows:

• If A is $p \in P$, then $\upsilon _{I,s} (A) = s(p).$.

• If A is ¬ A′ then $\upsilon _{I,s} (A) = T$ iff $\upsilon _{I,s} (A^\prime ) = F$.

• If A is A′∨A″ then $\upsilon _{I,s} (A) = T$ iff $\upsilon _{I,s} (A^\prime ) = T$ or $\upsilon _{I,s} (A^\prime\prime ) = T$, and similarly for the other Boolean operators.

• If A is □A′ then $\upsilon _{I,s} (A) = T$ iff $\upsilon _{I,s^\prime } (A^\prime ) = T$ for all states s′∈ρ(s).

• If A is ◊A′ then $\upsilon _{I,s} (A) = T$ iff $\upsilon _{I,s^\prime } (A^\prime ) = T$ for some state s′∈ρ(s).

The notation $s \vDash _I A$ is used for $\upsilon _{I,s} (A) = T$. When $I$ is clear from the context, it can be omitted s⊨A iff v _s (A)=T. ■

Example 13.11

Let us compute the truth value of the formula □p∨□q for each state s in Fig. 13.2.

• ρ(s ₀)={s ₁,s ₂}. Since s ₁⊨q and s ₂⊨q, it follows that s ₀⊨□q. By the semantics of ∨, s ₀⊨□p∨□q.

• s ₃∈ρ(s ₁), but $s_{3}\not\models p$ and $s_{3}\not\models q$, so $s_{1}\not\models\Box p$ and $s_{1}\not\models\Box q$. Therefore, $s_{1}\not\models \Box p \vee \Box q$.

• ρ(s ₂)={s ₁}. Since s ₁⊨p, we have s ₂⊨□p and s ₂⊨□p∨□q.

• s ₃∈ρ(s ₃). $s_{3}\not\models \Box p \vee \Box q$ by the same argument used for s ₁. ■

13.2.3 Satisfiability and Validity

The definition of semantic properties in PTL is more complex than it is in propositional or first-order logic, because an interpretation consists of both states and truth values.

Definition 13.12

Let A be a formula in PTL.

• A is satisfiable iff there is an interpretation $I = (S,\rho )$ for A and a state $s \in S$ such that $s \vDash _I A$.

• A is valid iff for all interpretations $I = (S,\rho )$ for A and for all states $s \in S$, $s \vDash _I A$. Notation: ⊨A. ■

Example 13.13

The analysis we did for the formula A=□p∨□q in Example 13.11 shows that A is satisfiable because $s_0 \vDash _I A$ or because $s_2 \vDash _I A$. The formulas A is not valid because $s_1 \nvDash _I A$ or because $s_3 \nvDash _I A$. ■

We leave it as an exercise to show that any valid formula of propositional logic is a valid formula of PTL, as is any substitution instance of a valid propositional formula obtained by substituting PTL formulas uniformly for propositional letters. For example, □p→(□q→□p) is valid since it is a substitution instance of the valid propositional formula A→(B→A).

There are other formulas of PTL that are valid because of properties of temporal logic and not as instances of propositional validities. We will prove the validity of two formulas directly from the semantic definition. The first establishes a duality between □ and ◊, and the second is the distribution of □ over →, similar to the distribution of ∀ over →.

Theorem 13.14

(Duality)

⊨□p↔¬ ◊¬ p.

Proof

Let $I = (S,\rho )$ be an arbitrary interpretation for the formula and let s be an arbitrary state in $S$. Assume that s⊨□p, and suppose that s⊨◊¬ p. Then there exists a state s′∈ρ(s) such that s′⊨¬ p. Since s⊨□p, for all states t∈ρ(s), t⊨p, in particular, s′⊨p, contradicting s′⊨¬ p. Therefore, s⊨¬ ◊¬ p. Since $I$ and s were arbitrary we have proved that ⊨□p→¬ ◊¬ p. We leave the converse as an exercise. ■

Theorem 13.15

⊨□(p→q)→(□p→□q).

Proof

Suppose, to the contrary, that there is an interpretation $I = (S,\rho )$ and a state s∈S, such that s⊨□(p→q) and s⊨□p, but s⊨¬ □q. By Theorem 13.14, s⊨¬ □q is equivalent to s⊨◊¬ q, so there exists a state s′∈ρ(s) such that s′⊨¬ q. By the first two assumptions, s′⊨p→q and s′⊨p, which imply s′⊨q, a contradiction. ■

13.3 Models of Time

In modal and temporal logics, different logics can be obtained by placing restrictions on the transition relation. In this section, we discuss the various restrictions, leading up to the ones that are appropriate for the temporal logics used in computer science. For each restriction on the transition relation, we give a formula that characterizes interpretations with that restriction. Proofs of the characterizations are given in a separate subsection.

Reflexivity

Definition 13.16

An interpretation $I = (S,\rho )$ is reflexive iff ρ is a reflexive relation: for all $s \in S$, (s,s)∈ρ, or s∈ρ(s) in functional notation. ■

Consider the formula ◊running, whose intuitive meaning is eventually the program is in the state ‘running’. Obviously, if a program is running now, then there is an reachable state (namely, now) in which the program is running. Thus it is reasonable to require that interpretations for properties of programs be reflexive.

Theorem 13.17

An interpretation with a reflexive relation is characterized by the formula □A→A (or, by duality, by the formula A→◊A).

Transitivity

Definition 13.18

An interpretation $I = (S,\rho )$ is transitive iff ρ is a transitive relation: for all $s_1 ,s_2 ,s_3 \in S$, $s_{2}\in\rho(s_{1}) \wedge s_{3}\in\rho(s_{2})\;\mathbin {\rightarrow }\; s_{3}\in\rho(s_{1}).$ ■

It is natural to require that interpretations be transitive. Consider a situation where we have proved that s ₁⊨◊running because s ₂⊨running for s ₂∈ρ(s ₁), and, furthermore, we have proved s ₂⊨◊running because s ₃⊨running for s ₃∈ρ(s ₂). It would be very strange if $s_{3}\not\in\rho(s_{1})$ and could not be used to prove s ₁⊨◊running.

Theorem 13.19

An interpretation with a transitive relation is characterized by the formula □A→□□A (or by the formula ◊◊A→◊A).

Example 13.20

In Fig. 13.2, ρ is not transitive since s ₁∈ρ(s ₂) and s ₃∈ρ(s ₁) but $s_{3}\not\in\rho(s_{2})$. This leads to the anomalous situation where s ₂⊨□p but $s_{2}\not\models \Box \Box p$. ■

Corollary 13.21

In an interpretation that both is reflexive and transitive, ⊨□A↔□□A and ⊨◊A↔◊◊A.

Linearity

Definition 13.22

An interpretation $I = (S,\rho )$ is linear if ρ is a function, that is, for all $s \in S$, there is at most one $s^\prime \in S$ such that s′∈ρ(s).

It might appear that a linear temporal logic would be limited to expressing properties of sequential programs and could not express properties of concurrent programs, where each state can have several possible successors depending on the interleaving of the statements of the processes. However, linear temporal logic is successful precisely in the context of concurrent programs because there is an implicit universal quantification in the definitions.

Suppose we want to prove that a program satisfies a correctness property expressed as a temporal logic formula like A=□◊running: in any state, the execution will eventually reach a state in which the computation is running. The program will be correct if this formula is true in every possible execution of the program obtained by interleaving the instructions of its processes. Each interleaving can be considered as a single linear interpretation, so if we prove $\vDash _I A$ for an arbitrary linear interpretation $I$, then the correctness property holds for the program.

Discreteness

Although the passage of time is often considered to be continuous and expressible by real numbers, the execution of a program is considered to be a sequence of discrete steps, where each step consists of the execution of a single instruction of the CPU. Thus it makes sense to express the concept of the next instant in time. To express discrete steps in temporal logic, an additional operator is added.

Definition 13.23

The unary operator $\bigcirc$ is called next.  ■

The definition of the truth value of a formula is extended as expected:

Definition 13.24

If A is $\bigcirc A^\prime$ then $\upsilon _{I,s} (A) = T$ iff $\upsilon _{I,s^\prime } (A^\prime ) = T$ for some s′∈ρ(s). ■

The next operator is self-dual in a linear interpretation.

Theorem 13.25

A linear interpretation whose relation ρ is a function is characterized by the formula $\bigcirc A \leftrightarrow \neg \bigcirc \neg A$.

The operator $\bigcirc$ plays a crucial role in the theory of temporal logic and in algorithms for deciding properties like satisfiability, but it is rarely used to express properties of programs. In a concurrent program, not much can be said about what happens next since we don’t know which operation will be executed in the next step. Furthermore, we want a correctness statement to hold regardless of how the interleaving selects a next operation. Therefore, properties are almost invariably expressed in terms of always and eventually, not in terms of next.

13.3.1 Proofs of the Correspondences *

The following definition enables us to talk about the structure (the states and transitions) of an entire class of interpretations while abstracting away from the assignment to atomic propositions in each state. A frame is obtained from an interpretation by ignoring the assignments in the states; conversely, a interpretation is obtained from a frame by associating an assignment with each state.

Definition 13.26

A frame $F$ is a pair $(W,\rho )$, where $W$ is a set of states and ρ is a binary relation on states. An interpretation $I = (S,\rho )$ is based on a frame $F = (W,\rho )$ iff there is a one-to-one mapping from $S$ onto $W$.

A PTL formula A characterizes a class of frames iff for every $F_i$ in the class, the set of interpretations $I$ based on $W$ is the same as the set of interpretations in which A is true. ■

Theorems 13.17, 13.19 and 13.25 are more precisely stated as follows: the formulas □A→A, □A→□□A and $\bigcirc A \leftrightarrow \neg \bigcirc \neg A$ characterize the sets of reflexive, transitive, and linear frames, respectively.

Proof of Theorem 13.17

Let $F_i$ be a reflexive frame, let $I$ be an arbitrary interpretation based on $F_i$, and suppose that $\nvDash _I \square A \to A$. Then there is a state $s \in S$ such that $s \vDash _I \square A$ and $s \nvDash _I A$. By the definition of □, for any state s′∈ρ(s), $s^\prime \vDash _I A$. By reflexivity, s∈ρ(s), so $s \vDash _I A$, a contradiction.

Conversely, suppose that $F_i$ is not reflexive, and let $s \in S$ be a state such that $s\not\in \rho(s)$. If ρ(s) is empty, □p is vacuously true in s; by assigning F to v _s (p), $s \nvDash _I \square p \to p$. If ρ(s) is non-empty, let $I$ be an interpretation based on $F_i$ such that v _s (p)=F and v _s′(p)=T for all s′∈ρ(s). These assignments are well-defined since $s\not\in \rho(s)$. Then $s \nvDash _I \square p \to p$.  ■

Proof of Theorem 13.19

Let $F_i$ be a transitive frame, let $I$ be an arbitrary interpretation based on $F_i$, and suppose that $\nvDash _I \square A \to \square \square A$. Then there is an $s \in S$ such that $s \vDash _I \square A$ and $s \nvDash _I \square \square A$. From the latter formula, there must be an s′∈ρ(s) such that $s^\prime \nvDash _I \square A$, and, then, there must be an s″∈ρ(s′) be such that $s^{\prime\prime} \nvDash _I A$. But $s \vDash _I \square A$, and by transitivity, s″∈ρ(s), so $s^{\prime\prime} \nvDash _I A$, a contradiction.

Conversely, suppose that $F_i$ is not transitive, and let $s,s^\prime ,s^{\prime\prime} \in S$ be states such that s′∈ρ(s), s″∈ρ(s′), but $s''\not\in\rho(s)$. Let $I$ be an interpretation based on $F_i$ which assigns T to p in all states in ρ(s) and F to p in s″, which is well-defined since $s''\not\in\rho(s)$. Then $s \vDash _I \square p$, but $s \nvDash _I \square \square p$. If there are only two states, s′ need not be distinct from s. A one state frame is necessarily transitive, possibly vacuously if the relation is empty. ■

We leave the proof of Theorem 13.25 as an exercise.

13.4 Linear Temporal Logic

In the context of programs, the natural interpretations of temporal logic formulas are discrete, reflexive, transitive and linear. There is another restriction that simplifies the presentation: the transition function must be total so that each state has exactly one next state. An interpretation for a computation that terminates in state s is assumed to have a transition from s to s.

Definition 13.27

Linear temporal logic (LTL) is propositional temporal logic whose interpretations are limited to transitions which are discrete, reflexive, transitive, linear and total. ■

These interpretations can be represented as infinite paths:

Since there is only one transition out of each state, it need not be explicitly represented, so interpretations in LTL are defined to be paths of states:

Definition 13.28

An interpretation for an LTL formula A is a path of states:

$$ \sigma = s_0, s_1, s_2, \ldots, $$

where each s _i is an assignment of truth values to the atomic propositions in A, $s_i :P \to \{ T,F\}$. Given σ, σ _i is the path that is the ith suffix of σ:

$$ \sigma_i = s_i, s_{i+1}, s_{i+2}, \ldots. $$

v _σ (A), the truth value of A in σ, is defined by structural induction:

• If A is $p \in P$, then v _σ (A)=s ₀(p).

• If A is ¬ A′ then v _σ (A)=T iff v _σ (A′)=F.

• If A is A′∨A″ then v _σ (A)=T iff v _σ (A′)=T or v _σ (A″)=T, and similarly for the other Boolean operators.

• If A is $p \in P$ then v _σ (A)=T iff $v_{\sigma_{1}}(A')=T$.

• If A is □A′ then v _σ (A)=T iff $v_{\sigma_{i}}(A')=T$ for all i≥0.

• If A is ◊A′ then v _σ (A)=T iff $v_{\sigma_{i}}(A')=T$ for some i≥0.

If v _σ (A)=T, we write σ⊨A. ■

Definition 13.29

Let A be a formula in LTL. A is satisfiable iff there is an interpretation σ for A such that σ⊨A. A is valid iff for all interpretations σ for A, σ⊨A. Notation: ⊨A.  ■

Definition 13.30

A formula of the form $\bigcirc A$ or $\neg \bigcirc A$ is a next formula. A formula of the form ◊A or ¬ □A is a future formula. ■

13.4.1 Equivalent Formulas in LTL

This section presents LTL formulas that are equivalent because of their temporal properties. Since any substitution instance of a formula in propositional logic is also an LTL formula, the equivalences in Sect. 2.3.3 also hold.

The equivalences are expressed in terms of an atom p but the intention is that they hold for arbitrary LTL formulas A.

The following formulas are direct consequences of our restriction of interpretations in LTL. The first three hold because interpretations are total, while the fourth holds because of linearity.

Theorem 13.31

$$ \begin{array}{*{20}c} { \vDash \square p \to \bigcirc p,} & { \vDash \bigcirc p \to \lozenge p,} & { \vDash \square p \to \lozenge p,} & { \vDash \bigcirc p \leftrightarrow \neg \bigcirc \neg p.} \\ \end{array} $$

Inductive

The following theorem is extremely important because it provides an method for proving properties of LTL formulas inductively.

Theorem 13.32

$$ \begin{array}{*{20}c} { \vDash \square p \leftrightarrow p \wedge \bigcirc \square p,} & { \vDash \lozenge p \leftrightarrow p \vee \bigcirc \lozenge p.} \\ \end{array} $$

These formulas can be easily understood by reading them in words: For a formula to be always true, p must be true today and, in addition, p must be always true tomorrow. For a formula to be true eventually, either p is true today or it must be true in some future of tomorrow.

We prove the first formula; the second follows by duality.

Proof

Let σ be an arbitrary interpretation and assume that σ⊨□p. By definition, σ _i ⊨p for all i≥0; in particular, σ ₀⊨p. But σ ₀ is the same as σ, so σ⊨p. If $\sigma \nvDash \bigcirc \square p$, then $\sigma_{1}\not\models \Box p$, so for some i≥1, $\sigma_{i}\not\models p$, contradicting σ⊨□p.

Conversely, assume that $\sigma \vDash p \wedge \bigcirc \square p$. We prove by induction that $\sigma_i \vDash p \wedge \bigcirc \square p$ for all i≥0. Since ⊨A∧B→A is a valid formula of propositional logic, we can conclude that σ _i ⊨p for all i≥0, that is, σ⊨□p.

The base case is immediate from the assumption since σ ₀=σ. Assume the inductive hypothesis that $\sigma_i \vDash p \wedge \bigcirc \square p$. By definition of the semantics of $\bigcirc$, σ _i+1⊨□p, that is, for all j≥i+1, σ _j ⊨p, in particular σ _i+1⊨p. Furthermore, for j≥i+2, σ _j ⊨p, so σ _i+2⊨□p and $\sigma _{\text{i + 1}} \vDash \bigcirc \square p$.  ■

Induction in LTL is based upon the following valid formula:

$$ \vDash \square (p \to \bigcirc p) \to (p \to \square p). $$

The base case is to show that p holds in a state. The inductive assumption is p and the inductive step is to show that $p \to \bigcirc p$. When these two steps have been performed, we can conclude that □p.

Instead of proving the following equivalences semantically as in Theorem 13.32, we will prove them deductively in Chap. 14. By the soundness of the deductive system, they are valid.

Distributivity

The operators □ and $\bigcirc$ distribute over conjunction:

$$ \begin{gathered} \vDash \square (p \wedge q) \leftrightarrow (\square p \wedge \square q), \hfill \\ \vDash \bigcirc (p \wedge q) \leftrightarrow (\bigcirc p \wedge \bigcirc q). \hfill \\ \end{gathered} $$

The next operator also distributes over disjunction because it is self-dual, but □ only distributes over disjunction in one direction:

$$ \begin{gathered} \vDash (\square p \vee \square q) \to \square (p \vee q), \hfill \\ \vDash \bigcirc (p \vee q) \leftrightarrow (\bigcirc p \vee \bigcirc q). \hfill \\ \end{gathered} $$

By duality, there are similar formulas for ◊:

$$ \begin{array}{l} \models\Diamond (p\vee q)\mathbin {\leftrightarrow }(\Diamond p\vee \Diamond q),\\[2pt] \models\Diamond (p\wedge q)\mathbin {\rightarrow }(\Diamond p\wedge \Diamond q). \end{array} $$

Similarly, □ and $\bigcirc$ distribute over implication in one direction, while $\bigcirc$ distributes in both directions:

$$ \begin{gathered} \vDash \square (p \to q) \to (\square p \to \square q), \hfill \\ \vDash (\lozenge p \to \lozenge q) \to \lozenge (p \to q), \hfill \\ \vDash \bigcirc (p \to q) \leftrightarrow (\bigcirc p \to \bigcirc q). \hfill \\ \end{gathered} $$

Example 13.33

Here is a counterexample to ⊨(◊p∧◊q)→◊(p∧q):

The atomic proposition p is true in even-numbered states, while q is true in odd-numbered states, but there is no state in which both are true. ■

Commutativity

The operator $\bigcirc$ commutes with □ and ◊, but □ and ◊ commute only in one direction:

$$ \begin{gathered} \vDash \square \bigcirc p \leftrightarrow \bigcirc \square p, \hfill \\ \vDash \lozenge \bigcirc p \leftrightarrow \bigcirc \lozenge p, \hfill \\ \vDash \lozenge \square p \to \square \lozenge p. \hfill \\ \end{gathered} $$

Be careful to distinguish between □◊p and ◊□p. The formula □◊p means infinitely often: p is not required to hold continuously, but at any state it will hold at some future state.

The formula ◊□p means for all but a finite number of states: in a path σ=s ₀,s ₁,s ₂,… , there is a natural number n such that p is true in all states in σ _n =s _n ,s _n+1,s _n+2,… .

Theorem 13.34

$\models(\Diamond \Box p \wedge \Box \Diamond q)\;\mathbin {\rightarrow }\;\Box \Diamond (p\wedge q)$.

Once p becomes always true, it will be true in the (infinite number of) states where q is true. We leave the proof as an exercise.

The diagram in Example 13.33 is also a counterexample to the formula: $\models(\Box \Diamond p \wedge \Box \Diamond q)\;\mathbin {\rightarrow }\;\Box \Diamond (p\wedge q)$.

Collapsing

In a formula without the $\bigcirc$ operator, no more than two temporal operators need appear in a sequence. A sequence of identical operators □ or ◊ is equivalent to a single occurrence and a sequence of three non-identical operators collapses to a pair of operators:

$$ \begin{array}{l} \models\Box \Box p\mathbin {\leftrightarrow }\Box p,\\[2pt] \models\Diamond\Diamond p \mathbin {\leftrightarrow }\Diamond p,\\[2pt] \models\Box \Diamond \Box p \mathbin {\leftrightarrow }\Diamond \Box p,\\[2pt] \models\Diamond \Box \Diamond p\mathbin {\leftrightarrow }\Box \Diamond p. \end{array} $$

13.5 Semantic Tableaux

The method of semantic tableaux is a decision procedure for satisfiability in LTL. The construction of a semantic tableau for a formula of LTL is more complex than that it is for a formula of propositional logic for two reasons:

First, to show that a formula in propositional logic is satisfiable, one need only find a single assignment to the atomic propositions that makes the formula evaluate to true. In LTL, however, there are many different assignments, one for each state. Therefore, we need to distinguish between ordinary nodes in the tableau used to decompose formulas such as p∧q and p∨q from nodes that represent different states. For example, if $\bigcirc p$ is to be true in state s, then p must be assigned T in the state s′ that follows s, but p could be assigned either T or F in s itself.

The second complication comes from future formulas like ◊p. For future formulas, it is not sufficient that they are consistent with the other subformulas; ◊p requires that there actually exist a subsequent state where p is assigned T. This is similar to the case of ∃xp(x) in first-order logic: we must demonstrate that a value a exists such that p(a) is true. In first-order logic, this was simple, because we just chose new constant symbols from a countable set. In LTL, to establish the existence or non-existence of a state that fulfills a future formula requires an analysis of the graph of states constructed when the tableau is built.

13.5.1 The Tableau Rules for LTL

The tableau rules for LTL consist of the rules for propositional logic shown in Fig. 2.8, together with the following new rules, where next formulas are called X-formulas:

The Rules for α- and β-Formulas

The rules for the α- and β-formulas are based on Theorem 13.32:

• If □A is true in a state s, then A is true in s and A must continue to be true in all subsequent states starting at the next state s′.

• If ◊A is true in a state s, then either A is true in s or A will eventually become true in some subsequent state starting at the next state s′.

The Rule for X-Formulas

Consider now the tableau obtained for the formula $A = (p \vee q) \wedge \bigcirc (\neg p \wedge \neg q)$ after applying the rules for α- and β-formulas:

In a model σ for A, either v _σ (p)=s ₀(p)=T or v _σ (q)=s ₀(q)=T, and this is expressed by the two leaf nodes that contain the atomic propositions. Since no more rules for α- and β-formulas are applicable, we have complete information on the assignment to atomic propositions in the initial state s ₀. These nodes, therefore, define states, indicated by the frame around the node.

These nodes contain additional information: in order to satisfy the formula A, the formula $\bigcirc (\neg p \wedge \neg q)$ must evaluate to T in σ ₀. Therefore, the formula ¬ p∧¬ q must evaluate to T in σ ₁. The application of the rule for X-formulas begins the construction of the new state s ₁:

The literals in s ₀ are not copied to the labels of the nodes created by the application of the rule for the X-formula because whatever requirements exist on the assignment in s ₀ are not relevant to what happens in s ₁.

On both branches, the new node is labeled by the formula ¬ p∧¬ q and an application of the rule for the propositional α-formula gives {¬ p,¬ q} as the label of the next node. Since this node no longer contains α- or β-formulas, it defines a new state s ₁.

The construction of the tableau is now complete and we have two open branches. Therefore, we can conclude that any model for A must be consistent with one of the following graphs:

This structure is not an interpretation. First, it is not total since there is no transition from s ₁, but this is easily fixed by adding a self-loop to the final state:

More importantly, we have not specified the value of the second literal in either of the possible states s ₀. However, the structures are Hintikka structures, which can be extended to interpretations by specifying the values of all atoms in each state.

Future Formulas

Consider the formula A=¬ (□(p∧q)→□p) which is the negation of a valid formula. Here is a semantic tableau, where (by duality) we have implicitly changed ¬ □ to ◊¬  for clarity:

The left-hand branch closes, while the right-hand leaf defines a state s ₀ in which p and q must be true. When rule for the X-formula is applied to this node, a new node is created that is labeled by $\{\Box (p\wedge q),\:\Diamond \neg \,p\}$. But this is the same set of formulas that labels the second node in the tableau. It is clear that the continuation of the construction will create an infinite structure:

Something is wrong since A is unsatisfiable and its tableau should close!

This structure is a Hintikka structure (no node contains clashing literals and for every α-, β- and X-formula, the Hintikka conditions hold). However, the structure cannot be extended to model for A, since the future subformula ◊¬ p is not fulfilled; that is, the structure promises to eventually produce a state in which ¬ p is true but defers forever the creation of such a state.

Finite Presentation of an Interpretation

There are only a finite number of distinct states in an interpretation for an LTL formula A since every state is labeled with a subset of the atomic propositions appearing in A and there are a finite number of such subsets. Therefore, although an interpretation is an infinite path, it can be finitely presented by reusing existing states instead of creating new ones. The infinite structure above can be finitely presented as follows:

13.5.2 Construction of Semantic Tableaux

The construction of semantic tableaux for LTL formulas and the proof of an algorithm for the decidability of satisfiability is contained in the following four subsections. First, we describe the construction of the tableau; then, we show how a Hintikka structure is defined by an open tableau; third, we extract a linear structure which can be extended to an interpretation; and finally, we show how to decide if future formulas are fulfilled.

The meaning of the following definition will become clear in the following subsection, but it is given here so that we can use it in the algorithm for constructing a tableau.

Definition 13.35

A state node in a tableau is a node l such that its label U(l) contains only literals and next formulas, and there are no complementary pairs of literals in U(l). ■

Algorithm 13.36

(Construction of a semantic tableau)

Input: An LTL formula A.

Output: A semantic tableau $T$ for A. Each node of $T$ is labeled with a set of formulas. Initially, $T$ consists of a single node, the root, labeled with the singleton set {A}. The tableau is built inductively as follows. Choose an unmarked leaf l labeled with a set of formulas U(l) and perform one of the following steps:

• If there is a complementary pair of literals {p,¬ p}⊆U(l), mark the leaf closed ×. If U(l) is a set of literals but no pair is complementary, mark the leaf open ⊙.

• If U(l) is not a set of literals, choose A∈U(l) which is an α-formula. Create a new node l′ as a child of l and label l′ with:

  $$U(l')=(U(l)-\{A\})\cup\{\alpha_{1},\alpha_{2}\}.$$

  (In the case that A is ¬ ¬ A ₁, there is no α ₂.)

• If U(l) is not a set of literals, choose A∈U(l) which a β-formula. Create two new nodes l′ and l″ as children of l. Label l′ with:

  $$U(l')=(U(l)-\{A\})\cup\{\beta_{1}\},$$

  and label l″ with:

  $$U(l'')=(U(l)-\{A\})\cup\{\beta_{2}\}.$$

• If l is a state node (Definition 13.35) with at least one next formula, let:

  $$ \{ \bigcirc A_1 , \ldots ,\bigcirc A_m ,\neg \bigcirc A_{m + 1} , \ldots ,\neg \bigcirc A_n \} $$

  be the set of next formulas in U(l). Create a new node l′ as a child of l and label l′ with:

  $$U(l')=\{A_{1},\ldots,A_{m},\neg \,A_{m+1},\ldots,\neg \,A_{n}\}.$$

  If U(l′)=U(l″) for a state node l″ that already exists in the tableau, do not create l′; instead connect l to l″.

The construction terminates when every leaf is marked × or ⊙. ■

We leave it as an exercise to show that the construction always terminates.

Definition 13.37

A tableau whose construction has terminated is a completed tableau. A completed tableau is closed if all leaves are marked closed and there are no cycles. Otherwise, it is open. ■

Example 13.38

Here is a completed open semantic tableau with no leaves:

 ■

13.5.3 From a Semantic Tableau to a Hintikka Structure

The next step is to construct a structure from an open tableau, to define the conditions for a structure to be a Hintikka structure and to prove that the structure resulting from the tableau satisfies those conditions. The definition of a structure is similar to the definition of an interpretation for PTL formulas (Definition 13.8); the difference is that the labels of a state are sets of formulas, not just sets of atomic propositions that are assigned true. To help understand the construction, you might want to refresh your memory by re-reading Sect. 2.7.2 on the definition and use of Hintikka structures in propositional logic.

Definition 13.39

A structure $H$ for a formula A in LTL is a pair $(S,\rho )$, where $S = \{ s_1 , \ldots ,s_n \}$ is a set of states each of which is labeled by a subset of formulas built from the atomic propositions in A and ρ is a binary relation on states, ρ⊆S×S. ■

As before, functional notation may be used s ₂∈ρ(s ₁).

The states of the structure will be the state nodes of the tableau. However, the labels of the states must include more than the literals that label the nodes in the tableau. To obtain a Hintikka structure, the state in the structure must also include the formulas whose decomposition eventually led to each literal.

Example 13.40

In Example 13.38, state node l ₂ will define a state in the structure that is labeled with p, since p must be assigned true in any interpretation containing that state. In addition, the state in the structure must also include ◊p from l ₁ (because p in l ₂ resulted from the decomposition of ◊p), as well as □◊p from l ₀ (because ◊p in l ₁ resulted from the decomposition of □◊p). ■

The transitions in the structure are defined by paths between state nodes.

Definition 13.41

A state path is a path (l ₀,l ₁,…,l _k−1,l _k ) through connected nodes in the tableau, such that l ₀ is a state node or the root of the tableau, l _k is a state node, and none of {l ₁,…,l _k−1} are state nodes. It is possible that l ₀=l _k so that the set {l ₁,…,l _k−1} is empty. ■

Given a tableau, a structure can be defined by taking the state nodes as the states and defining the transitions by the state paths. The label of a state is the union of all formulas that appear on incoming state paths (not including the first state of the path unless it is the root). The formal definition is:

Definition 13.42

Let $T$ be an open tableau for an LTL formula A. The structure $H$ constructed from $T$ is:

• $S$ is the set of state nodes.

• Let $s \in S$. Then s=l for some node l in the tableau. Let $\pi^{i}=(l^{i}_{0},l^{i}_{1},\ldots,l^{i}_{k_{i}}=l)$ be a state path terminating in the node l and let:

  $$U^i=U(l^i_{1})\cup\cdots\cup U(l^i_{k_i})$$

  or

  $$U^i=U(l^i_{0})\cup\cdots\cup U(l^i_{k_i})$$

  if $l^{i}_{0}$ is the root. Label s by the set of formulas:

  $$U_{i}=\cup_{i}U^i,$$

  where the union is taken over all i such that π ⁱ is a state path terminating in l=s.

• s′∈ρ(s) iff there is a state path from s to s′. ■

It is possible to obtain several disconnected structures from the tableau for a formula such as ◊p∨◊q, but this is no problem as the formula can be satisfiable if and only if at least one of the structures leads to a model.

Now that we know how the structure is constructed from the tableau, it is possible to optimize Algorithm 13.36. Change:

For a state node l′, if U(l′)=U(l″) for a state node l″ that already exists in the tableau, do not create l′; instead connect l to l″.

so that it applies to any node l′ in the tableau, not just to state nodes, provided that this doesn’t create a cycle not containing a state node.

Example 13.43

Here is an optimized tableau corresponding to the one in Example 13.38:

and here is the structure constructed from this semantic tableau:

where s ₀=l ₂ and s ₁=l ₃. To save space, each state s _i is labeled only with the positive literals in U _i . ■

Example 13.44

Let:

$$A=\Box (\Diamond (p\wedge q)\wedge \Diamond (\neg \,p\wedge q) \wedge \Diamond (p\wedge \neg \,q)).$$

The construction of the tableau for A is left as an exercise. The structure obtained from the tableau is shown in Fig. 13.3. ■

Fig. 13.3

Structure for □(◊(p∧q)∧◊(¬ p∧q)∧◊(p∧¬ q))

Definition 13.45

Let $H = (S,\rho )$ be a structure for an LTL formula A. $H$ is a Hintikka structure for A iff A∈s ₀ and for all states s _i the following conditions hold for U _i , the set of formulas labeling s _i :

• 1. For all atomic propositions p in A, either $p\not\in U_{i}$ or $\neg \,p\not\in U_{i}$.

• 2. If α∈U _i , then α ₁∈U _i and α ₂∈U _i .

• 3. If β∈U _i , then β ₁∈U _i or β ₂∈U _i .

• 4. If X∈U _i , then for all s _j ∈ρ(s _i ), X ₁∈U _j . ■

Theorem 13.46

Let A be an LTL formula and suppose that the tableau $T$ for A is open. Then the structure $H$ created as described in Definition 13.42 is a Hintikka structure for A.

Proof

The structure $H$ is created from an open tableau, so condition (1) holds. Rules for α- and β-formulas are applied before rules for next formulas, so the union of the formulas on every incoming state path to a state node contains all the formulas required by conditions (2) and (3). When the rule for a next formula $H$ is applied, A will appear in the label of the next node (and similarly for $\neg \bigcirc A$), and hence in every state at the end of a state path that includes this node. ■

13.5.4 Linear Fulfilling Hintikka Structures

The construction of the tableau and the Hintikka structure is quite straightforward given the decomposition of formulas with temporal operators. Now we turn to the more difficult problem of deciding if an interpretation for an LTL formula can be extracted from a Hintikka structure. First, we need to extract a linear structure and show that it is also a Hintikka structure.

Definition 13.47

Let $H$ be a Hintikka structure for an LTL formula A. $H$ is a linear Hintikka structure iff ρ is a total function, that is, if for each s _i there is exactly one s _j ∈ρ(s _i ). ■

Lemma 13.48

Let $H$ be a Hintikka structure for an LTL formula A and let $H^\prime$ be an infinite path through $H$. Then $H^\prime$ is a linear Hintikka structure.

Proof

Clearly, $H^\prime$ is a linear structure. Conditions (1–3) of Definition 13.45 hold because they already held in $H$. Let s be an arbitrary state and let U be the label of s. If a next formula $\bigcirc A^\prime$ occurs in U, then by condition (4) of Definition 13.45, A′ occurs in all states of ρ(s), in particular, for the one chosen in the construction of $H^\prime$. ■

Next, we need to check if the linear structure fulfills all the future formulas. We define the concept of fulfilling and then show that a fulfilling Hintikka structure can be used to define a model. The algorithm for deciding if a Hintikka structure is fulfilling is somewhat complex and is left to the next subsection. To simplify the presentation, future formulas will be limited to those of the form ◊A. By duality, the same presentation is applicable to future formulas of the form ¬ □A.

Recall that ρ is the transitive, reflexive closure of ρ (Definition A.21).

Definition 13.49

Let $H = (S,\rho )$ be a Hintikka structure. $H$ is a fulfilling iff the following condition holds for all future formulas ◊A:

For all $s \in S$, if ◊A∈U _s , then for some s′∈ρ ^∗(s), A∈U _s′.

The state s′ is said to fulfill ◊A. ■

Theorem 13.50

(Hintikka’s Lemma for LTL)

Let $H = (S,\rho )$ be a linear fulfilling Hintikka structure for an LTL formula A. Then A is satisfiable.

Proof

An LTL interpretation is a path consisting of states labeled with atomic propositions (see Definition 13.28). The path is defined simply by taking the linear Hintikka structure and restricting the labels to atomic propositions. There is thus a natural mapping between states of the interpretation and states of the Hintikka structure, so for the propositional operators and next formulas, we can use the conditions on the structure to prove that A is satisfiable using structural induction.

For future formulas, the satisfiability follows from the assumption that the Hintikka structure is fulfilling.

Consider now a formula of the form $\Box A\in U_{s_{i}}$. We must show that $v_{\sigma_{j}}(A)=T$ for all j≥i. We generalize this for the inductive proof and show that $v_{\sigma_{j}}(A)=T$ and $\upsilon _{\sigma _j } (\bigcirc \square A) = T$ for all j≥i.

The base case is j=i. But $\Box A\in U_{s_{i}}$, so by Hintikka condition (2) $A\in U_{s_{i}}$ and $\bigcirc \square A \in U_{si}$.

Let k≥i and assume the inductive hypothesis that $v_{\sigma_{k}}(A)=T$ and $\bigcirc \square A \in U_{sk}$. By Hintikka condition (4), $\Box A\in U_{s_{k+1}}$, so using Hintikka condition (2) again, $v_{\sigma_{k+1}}(A)=T$ and $\bigcirc \square A \in U_{sk + 1}$. ■

Here is a finite presentation of a linear fulfilling Hintikka structure constructed from the structure in Fig. 13.3:

13.5.5 Deciding Fulfillment of Future Formulas *

The last link needed to obtain a decision procedure for satisfiability in LTL is an algorithm that takes an arbitrary Hintikka structure, and decides if it contains a path that is a linear fulfilling Hintikka structure. We begin with some definitions from graph theory. The concepts should be familiar, though it is worthwhile giving formal definitions.

Definition 13.51

A graph G=(V,E) consists of a set of vertices V={v ₁,…,v _n } and a set of edges E={e ₁,…,e _m }, which are pairs of vertices e _k ={v _i ,v _j }⊆V. In a directed graph, each edge is an ordered pair, e _k =(v _i ,v _j ). A path from v to v′, denoted v⇝v′, is a sequence of edges such that the second component of one edge is the first component of the next:

$$ \begin{array}{r@{\ \ \ }l@{\ \ \ }l} e_{1}&=&( v=v_{i_{1}},v_{i_{2}}),\:\\[2pt] e_2&=&(v_{i_{2}},v_{i_{3}}),\:\\[2pt] &\ldots&\\[2pt] e_{l-1}&=&(v_{i_{l-2}},v_{i_{l-1}}),\:\\[2pt] e_{l}&=&(v_{i_{l-1}},v_{i_{l}}=v'). \end{array} $$

A subgraph G′=(V′,E′) of a directed graph G=(V,E) is a graph such that V′⊆V and E′⊆E, provided that e=(v _i ,v _j )∈E′ implies {v _i ,v _j }⊆V′. ■

Definition 13.52

A strongly connected component (SCC) G′=(V′,E′) in a directed graph G is a subgraph such that v _i ⇝v _j for all {v _i ,v _j }⊆V′. A maximal strongly connected component (MSCC) is an SCC not properly contained in another. A transient SCC is an MSCC consisting of a single vertex. A terminal SCC is an MSCC with no outgoing edges. ■

Example 13.53

The directed graph in Fig. 13.4 contains three strongly connected components: G ₀={s ₀},G ₁={s ₁,s ₂,s ₃},G ₂={s ₄,s ₅,s ₆,s ₇}. G ₀ is transient and G ₁ is terminal. ■

Fig. 13.4

Strongly connected components

Definition 13.54

A directed graph G can be represented as a component graph, which is a directed graph whose vertices are the MSCCs of G and whose edges are edges of G pointing from a vertex of one MSCC to a vertex of another MSCC. ■

See Even, Sect. 3.4 for an algorithm that constructs the component graph of a directed graph and a proof of the following theorem.

Theorem 13.55

The component graph is acyclic.

Example 13.56

Figure 13.5 shows the graph of Fig. 13.4 with its component graph indicated by ovals and thick arrows. ■

Fig. 13.5

Component graph

Suppose that we have a Hintikka structure and a future formula in a terminal MSCC, such as G ₁ in Fig. 13.5. Then if the formula is going to be fulfilled at all, it will be fulfilled within the terminal MSCC because there are no other reachable nodes to which the fulfillment can be deferred. If a future formula is in a non-terminal MSCC such as G ₂, it can either be fulfilled within its own MSCC, or the fulfillment can be deferred to an reachable MSCC, in this case G ₁. This suggests an algorithm for checking fulfillment: start at terminal MSCCs and work backwards.

Let $H = (S,\rho )$ be a Hintikka structure. $H$ can be considered a graph G=(V,E), where V is $S$ and (s _i ,s _j )∈E iff s _j ∈ρ(s _i ). We simplify the notation and write A∈v for A∈U _i when v=s _i .

Definition 13.57

Let G=(V,E) be a SCC of $H$. G is self-fulfilling iff for all v∈V and for all future formulas ◊A∈v, A∈v′ for some v′∈V. ■

Lemma 13.58

Let G=(V,E)⊆G′=(V′,E′) be SCCs of a Hintikka structure. If G is self-fulfilling, then so is G′.

Example 13.59

Let ◊A be an arbitrary future formula that has to be fulfilled in G′ in Fig. 13.6. If ◊A∈s _i for s _i ∈G, then by the assumption that G is self-fulfilling, A∈s _j for some s _j ∈G⊂G′ and G′ is also self-fulfilling.

Fig. 13.6

An SCC is contained in an MSCC

Suppose now that ◊A∈s ₇, where s ₇∈V′−V. If A∈s ₇, then s ₇ itself fulfills ◊A. Otherwise, by Hintikka condition (3), $\bigcirc \lozenge A \in s_7$, so ◊A∈s ₆ by Hintikka condition (4). Continuing, A∈s ₆ or $\bigcirc \lozenge A \in s_6$; A∈s ₄ or $\bigcirc \lozenge A \in s_4$; A∈s ₅ or $\bigcirc \lozenge A \in s_5$. If A∈s _j for one of these vertices in V′−V, we have the G′ is self-fulfilling.

If not, then by Hintikka condition (4), $\bigcirc \lozenge A \in s_4$ implies that ◊A∈s ₁, because condition (4) is a requirement on all immediate successors of a node. By assumption, G is self-fulfilling, so A∈s _j for some s _j ∈G⊂G′ and G′ is also self-fulfilling. ■

Proof of Lemma 13.58

Let ◊A be an arbitrary future formula in v′∈V′−V. By definition of a Hintikka structure, either A∈v′ or $\bigcirc \lozenge A \in \upsilon ^\prime$. If A∈v′, then A is fulfilled in G′; otherwise, ◊A∈v″ for every v″∈ρ(v′). By induction on the number of vertices in V′−V, either A is fulfilled in V′−V or ◊A∈v for some v in V. But G is self-fulfilling, so ◊A is fulfilled in some state v _A ∈V⊆V′. Since G′ is an SCC, v′⇝v _A and A is fulfilled in G′. ■

Corollary 13.60

Let G be a self-fulfilling SCC of a Hintikka structure. Then G can be extended to a self-fulfilling MSCC.

Proof

If G itself is not an MSCC, create a new graph G′ by adding a vertex v′∈V′−V and all edges (v′,v) and (v,v′), where v∈V, provided that G′ is an SCC. Continue this procedure until no new SCCs can be created. By Lemma 13.58, the SCC is self-fulfilling and by construction it is maximal. ■

Lemma 13.61

Let G=(V,E) be an MSCC of $H$ and let ◊A∈v∈V be a future formula. If G is not self-fulfilling, ◊A can only be fulfilled by some v′ in an MSCC G′, such that G⇝G′ in the component graph.

Proof

Since G is not self-fulfilling, ◊A must be fulfilled by some $v'\not\in V$ such that v⇝v′. But $v'\not\leadsto v$, otherwise v′ could be added to the vertices of G creating a larger SCC, contradicting the assumption that G is maximal. Therefore, v′∈G′ for a component G′≠G. ■

This lemma directly gives the following corollary.

Corollary 13.62

If G is a terminal MSCC and ◊A∈v for v∈V, then if ◊A cannot be fulfilled in G, it cannot be fulfilled at all.

Algorithm 13.63

(Construction of a linear fulfilling structure)

Input: A Hintikka structure $H$.

Output: A linear fulfilling Hintikka structure that is a path in $H$, or a report that no such structure exists.

Construct the component graph H of $H$. Since H is acyclic (Theorem 13.55), there must be a terminal MSCC G. If G is not self-fulfilling, delete G and all its incoming edges from H. Repeat until every terminal MSCC is self-fulfilling or until the component graph is empty. If every terminal MSCC is self-fulfilling, the proof of the following theorem shows how a linear fulfilling Hintikka structure can be constructed. Otherwise, if the graph is empty, the algorithm reports that no linear fulfilling Hintikka structure exists. ■

Theorem 13.64

Algorithm 13.63 terminates with a non-empty graph iff a linear fulfilling Hintikka structure can be constructed.

Proof

Suppose that the algorithm terminates with an non-empty component graph G and let G ₁⇝⋯⇝G _n be a maximal path in G. We now define a path in $H$ based upon this path in the component graph.

There must be vertices {v ₁,…,v _n } in $H$, such that v _i ∈G _i ,v _i+1∈G _i+1 and v _i ⇝v _i+1. Furthermore, each component G _i is an SCC, so for each i there is a path $v^{i}_{1} \leadsto \cdots \leadsto v^{i}_{k_{i}}$ in $H$ containing all the vertices in G _i .

Construct a path in $H$ by replacing every component by a partial path and connecting them by the edges v _i ⇝v _i+1:

• Replace a transient component by the single vertex $v^{i}_{1}$.

• Replace a terminal component by the closure

  $$v_{i}\leadsto \cdots \leadsto (v^{i}_{1} \leadsto \cdots \leadsto v^{i}_{k_{i}})^{*}.$$

• Replace a non-transient, non-terminal component by

  $$ v_{i}\leadsto \cdots \leadsto v^{i}_{1} \leadsto \cdots v^{i}_{k_{i}} \leadsto v^{i}_{1} \leadsto \cdots v^{i}_{k_{i}} \leadsto \cdots \leadsto v_{i+1}. $$

We leave it as an exercise to prove that this path is a fulfilling linear Hintikka structure.

Conversely, let $H^\prime = (s_1 , \ldots , \ldots )$ be a fulfilling linear Hintikka structure in $H$. Since $H$ is finite, some suffix of $H^\prime$ must be composed of states which repeat infinitely often. These states must be contained within a self-fulfilling SCC G. By Corollary 13.60, G is contained in a self-fulfilling MSCC. ■

Example 13.65

There are two maximal paths in the component graph in Fig. 13.5: G ₀⇝G ₁ and G ₀⇝G ₂⇝G ₁. The paths constructed in the underlying graphs are:

$$ s_{0}\leadsto (s_{3}\leadsto s_{2}\leadsto s_{1})^{*} $$

and

$$ s_{0}\leadsto s_{4}\leadsto s_{5}\leadsto s_{7}\leadsto s_{6}\leadsto s_{4}\leadsto s_{5}\leadsto s_{7}\leadsto s_{6}\leadsto s_{4} \leadsto (s_{1}\leadsto s_{2}\leadsto s_{3})^{*}, $$

respectively. ■

Theorem 13.66

There is a decision procedure for satisfiability in LTL.

Proof

Let A be a formula in LTL. Construct a semantic tableau for A. If it closes, A is unsatisfiable. If there is an open branch, A is satisfiable. Otherwise, construct the structure from the tableau as described in Definition 13.42. By Theorem 13.46, this is a Hintikka structure. Apply Algorithm 13.63 to construct a fulfilling Hintikka structure. If the resulting graph is empty, A is unsatisfiable. Otherwise, apply the construction in Theorem 13.64 to construct a linear fulfilling Hintikka structure. By Theorem 13.50, a model can be constructed from the structure. ■

The following corollary is obvious since the number of possible states in a structure constructed for a particular formula is finite:

Corollary 13.67

(Finite model property)

A formula in LTL is satisfiable iff it is satisfiable in a finitely-presented model.

13.6 Binary Temporal Operators *

Consider the following correctness specification from the introduction:

The output lines maintain their values until the set-line is asserted.

We cannot express this in LTL as defined above because we have no binary temporal operators that can connect two propositions: unchanged-output and set-asserted. To express such properties, a binary operator $U$ (read until) can be added to LTL. Infix notation is used:

$$ unchanged\text{ - }output\,\,U\,\,set\text{ - }asserted. $$

The semantics of the operator is defined by adding the following item to Definition 13.28:

• If A is $A_1 UA_2$ then v _σ (A)=T iff $v_{\sigma_{i}}(A_{2})=T$ for some i≥0 and for all 0≤k<i, $v_{\sigma_{k}}(A_{1})=T$.

Example 13.68

The formula $pUq$ is true in the interpretation represented by the following path:

q is true at s ₂ and for all previous states {s ₀,s ₁}, p is true.

$pUq$ is not true in the following interpretation assuming that state s ₂ is repeated indefinitely:

The reason is that q never becomes true. $pUq$ is also not true in the following interpretation:

because p becomes false before q becomes true. ■

Defining the Existing Operators in Terms of $U$

It is easy to see that:

$$ \lozenge A \equiv true\,UA. $$

The definition of the semantics of $U$ requires that A become true eventually just as in the semantics of ◊A. The additional requirement is that true evaluate to T in every previous state, but that clearly holds in every interpretation.

Since binary operators are essential for expressing correctness properties, advanced presentations of LTL take $\bigcirc$ and $U$ as the primitive operators of LTL and define ◊ as an abbreviation for the above formula, and then □ as an abbreviation for ¬ ◊¬ .

Semantic Tableaux with $U$

Constructing a semantic tableau for a formula that uses the $U$ operator does not require any new concepts. The operator can be decomposed as follows:

$$ A_1 UA_2 \equiv A_2 \vee (A_1 \wedge \bigcirc (A_1 UA_2 )). $$

For $A_1 UA_2$ to be true, either A ₂ is true today, or we put off to tomorrow the requirement to satisfy $A_1 UA_2$, while requiring that A ₁ be true today. The decomposition shows that a $U$-formula is a β-formula very similar to ◊A. The similarity goes deeper, because $A_1 UA_2$ is a future formula and must be fulfilled by having A ₂ appear in a state eventually.

The construction of semantic tableau is more efficient if operators have duals. The dual of $U$ is the operator $R$ (read release), defined as:

$$ A_1 RA_2 \equiv \neg (\neg A_1 U\neg A_2 ). $$

We leave it as an exercise to write the definition of the semantics of $R$.

The Weak Until Operator

Sometimes it is convenient to express precedence properties without actually requiring that something eventually occur. $W$ (read weak until) is the same as the operator $U$ except that it is not required that the second formula ever become true:

• If A is $A_1 WA_2$ then v _σ (A)=T iff: if $v_{\sigma_{i}}(A_{2})=T$ for some i≥0, then for all 0≤k<i, $v_{\sigma_{k}}(A_{1})=T$.

Clearly, the following equivalence holds:

$$ A_1 WA_2 \equiv (A_1 UA_2 ) \vee \square A_1 . $$

We leave it as an exercise to show:

$$ \begin{array}{*{20}l} {\square A} & \equiv & {A\,W\,false,} \\ {\neg (A_1 WA_2 )} & \equiv & {(A_1 \wedge \neg A_2 )U(\neg A_1 \wedge \neg A_2 ),} \\ {\neg (A_1 UA_2 )} & \equiv & {(A_1 \wedge \neg A_2 )W(\neg A_1 \wedge \neg A_2 ),} \\ {\neg (A_1 UA_2 )} & \equiv & {(\neg A_2 )W(\neg A_1 \wedge \neg A_2 ).} \\ \end{array} $$

13.7 Summary

Since the state of a computation changes over time, temporal logic is an appropriate formalism for expressing correctness properties of programs. The syntax of linear temporal logic (LTL) is that of propositional logic together with the unary temporal operators □, ◊, $\bigcirc$. Interpretations are infinite sequences of states, where each state assigns truth values to atomic propositions. The meaning of the temporal operators is that some property must hold in □ all subsequent states, in ◊ some subsequent state or in the $\bigcirc$ next state.

Satisfiability and validity of formulas in LTL are decidable. The tableau construction for propositional logic is extended so that next formulas (of the form $\bigcirc A$) cause new states to be generated. A open tableau defines a Hintikka structure which can be extended to a satisfying interpretation, provided that all future formulas (of the form ◊A or ¬ □A) are fulfilled. By constructing the component graph of strongly connected components, the fulfillment of the future formulas can be decided.

Many important correctness properties use the binary operators $U$ and $W$, which require that one formula hold until a second one becomes true.

13.8 Further Reading

Temporal logic (also called tense logic) has a long history, but it was first applied to program verification by Pnueli (1977). The definitive reference for the specification and verification of concurrent programs using temporal logic is Manna and Pnueli (1992, 1995). The third volume was never completed, but a partial draft is available (Manna and Pnueli, 1996). Modern treatments of LTL can be found in Kröger and Merz (2008, Chap. 2), and Baier and Katoen (2008, Chap. 5). The tableau method for a different version of temporal logic first appeared in Ben-Ari et al. (1983); for a modern treatment see Kröger and Merz (2008, Chap. 2).

13.9 Exercises

13.1

Prove that in LTL every substitution instance of a valid propositional formula is valid.

13.2

Prove ⊨¬ ◊¬ p→□p (the converse direction of Theorem 13.14).

13.3

Prove that a linear interpretation is characterized by $\bigcirc A \leftrightarrow \neg \bigcirc \neg A$ (Theorem 13.25).

13.4

* Identify the property of a reflexive relation characterized by A→□◊A. Identify the property of a reflexive relation characterized by ◊A→□◊A.

13.5

Show that in an interpretation with a reflexive transitive relation, any formula (without $\bigcirc$) is equivalent to one whose only temporal operators are □, ◊, ◊□, □◊, ◊□◊ and □◊□. If the relation is also characterized by the formula ◊A→□◊A, any formula is equivalent to one with a single temporal operator.

13.6

Prove Theorem 13.34: $\models(\Diamond \Box p \wedge \Box \Diamond q)\;\mathbin {\rightarrow }\;\Box \Diamond (p\wedge q)$.

13.7

Construct a tableau and find a model for the negation of □◊p→◊□p.

13.8

Prove that the construction of a semantic tableau terminates.

13.9

Prove that the construction of the path in the proof of Theorem 13.64 gives a linear fulfilling Hintikka structure.

13.10

Write the definition of the semantics of the operator $R$.

13.11

Prove the equivalences on $W$ at the end of Sect. 13.6.