Temporal Logic: A Deductive System

Abstract

This chapter defines the deductive system $L$ for linear temporal logic. We will prove many of the formulas presented in the previous chapter, as well as the soundness and completeness of $L$.

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.

This chapter defines the deductive system $L$ for linear temporal logic. We will prove many of the formulas presented in the previous chapter, as well as the soundness and completeness of $L$.

14.1 Deductive System $L$

The operators of $L$ are the Boolean operators of propositional logic together with the temporal operators □ and $\bigcirc$. The operator ◊ is defined as an abbreviation for ¬ □¬ .

Definition 14.1

The axioms of $L$ are:

$$ \begin{array}{*{20}l} {\mathbf{Axiom}\,\mathbf{0}} & {\mathbf{Prop}} & {\text{Any}\,\text{substitution}\,\text{instance}\,\text{of}} \\ {} & {} & {\text{a}\,\text{valid}\,\text{propositional}\,\text{formula}\text{.}} \\ {\mathbf{Axiom}\,\mathbf{1}} & {\mathbf{Distribution}\,\mathbf{of}\,\square } & { \vdash \square (A \to B) \to (\square A \to \square B).} \\ {\mathbf{Axiom}\,\mathbf{2}} & {\mathbf{Distribution}\,\mathbf{of}\,\bigcirc } & { \vdash \bigcirc (A \to B) \to (\bigcirc A \to \bigcirc B).} \\ {\mathbf{Axiom}\,\mathbf{3}} & {\mathbf{Expansion}\,\mathbf{of}\,\square } & { \vdash \square A \to (A \wedge \bigcirc A \wedge \bigcirc \square A).} \\ {\mathbf{Axiom}\,\mathbf{4}} & {\mathbf{Induction}} & { \vdash \square (A \to \bigcirc A) \to (A \to \square A).} \\ {\mathbf{Axiom}\,\mathbf{5}} & {\mathbf{Linearity}} & { \vdash \bigcirc A \leftrightarrow \neg \bigcirc \neg A.} \\ \end{array} $$

The rules of inference are modus ponens and generalization: $\displaystyle \frac{\vdash A}{\vdash \Box A}.$ ■

In order to simplify proofs of formulas in LTL, the deductive system $L$ takes all substitution instances of valid formulas of propositional logic as axioms. Validity in propositional logic is decidable and by the completeness of $H$ we can produce a proof of any valid formula if asked to do so. In fact, we will omit justifications of deductions in propositional logic and just write Prop if a step in a proof is justified by propositional reasoning.

The distributive axioms are valid in virtually all modal and temporal logics (Theorem 13.15). The expansion axiom expresses the basic properties of □ that were used to construct semantic tableaux, as well as $\vdash \square A \to \bigcirc A$ (Theorem 13.25), which holds because all interpretations are infinite paths. The linearity axiom for $\bigcirc$ (Theorem 13.25) captures the restriction of LTL to linear interpretations.

The induction axiom is fundamental in $L$: since interpretations in LTL are infinite paths, proofs of non-trivial formulas usually require induction. In a proof by induction, the inductive step is $A \to \bigcirc A$, that is, we assume that A is true today and prove that A is true tomorrow. If this inductive step is always true, $\square (A \to \bigcirc A)$, then A→□A by the induction axiom. Finally, if A is true today (the base case), then A is always true □A.

The rules of inference are the familiar modus ponens and generalization using □, which is similar to generalization using ∀ in first-order logic.

Derived Rules

Here are some useful derived rules:

$$ \begin{array}{*{20}c} {\frac{{ \vdash A \to B}} {{ \vdash \square A \to \square B}},} & {\frac{{ \vdash A \to B}} {{ \vdash \bigcirc A \to \bigcirc B}},} & {\frac{{ \vdash A \to \bigcirc A}} {{ \vdash A \to \square A}}.} \\ \end{array} $$

The first is obtained by applying generalization and then the distribution axiom; the second is similar except that the expansion axiom is used between the generalization and the distribution. When using these rules, we write the justification as generalization. The third rule will be called induction because it is a shortcut for generalization followed by the induction axiom.

14.2 Theorems of $L$

The theorems and their proofs will be stated and proved for atomic propositions p and q although the intention is that they hold for arbitrary LTL formulas.

Distributivity

This subsection explores in more detail the distributivity of the temporal operators over proposition operators. The results will not be surprising, because □ and ◊ behave similarly to ∀ and ∃ in first-order logic. $\bigcirc$ is a special case because of linearity.

Theorem 14.2

$\vdash \bigcirc (p \wedge q) \leftrightarrow (\bigcirc p \wedge \bigcirc q)$.

Proof

 ■

By linearity, $\bigcirc$ is self-dual, while ∨ is the dual of ∧, so we immediately have $\vdash \bigcirc (p \vee q) \leftrightarrow (\bigcirc p \vee \bigcirc q)$.

Theorem 14.3

(Distribution)

⊢□(p∧q)↔(□p∧□q).

The proof of the forward implication ⊢□(p∧q)→(□p∧□q) is similar to that of Theorem 14.2 and is left as an exercise. Before proving the converse, we need to prove the converse of the expansion axiom; the proof uses the forward implication of Theorem 14.3, which we assume that you have already proved.

Theorem 14.4

(Contraction)

$\vdash p \wedge \bigcirc \square p \to \square p$.

Proof

 ■

For symmetry with the expansion axiom, $\bigcirc p$ could have been included in the premise of this theorem, but it is not needed.

Now we can prove the converse of Theorem 14.3. The structure of the proof is typical of inductive proofs in $L$. An explanation of some of the more difficult steps of the formal proof is given at its end.

Proof

Let r=□p∧□q∧¬ □(p∧q).

   ■

Steps 1–7 prove that r is invariant, meaning that r is true initially and remains true in any interpretation. The second line of Step 1 is justified by the contrapositive of contraction $\neg (p \wedge q) \to \neg ((p \wedge q) \wedge \bigcirc \square (p \wedge q))$. Step 3 follows from Step 2 because ¬ (p∧q) is inconsistent with p and q that must be true by the expansion of □p and □q.

The operator □ distributes over disjunction only in one direction. We leave the proof as an exercise, together with the task of showing that the converse is not valid.

Theorem 14.5

(Distribution)

⊢(□p∨□q)→□(p∨q).

Transitivity of □

Induction is used to prove that □ is transitive.

Theorem 14.6

(Transitivity)

⊢□□p↔□p

Proof

 ■

Commutativity

Another expected result is that □ and $\bigcirc$ commute:

Theorem 14.7

(Commutativity)

$\vdash \square \bigcirc p \leftrightarrow \bigcirc \square p$.

Proof

 ■

□ and ◊ commute in only one direction.

Theorem 14.8

⊢◊□p→□◊p.

We leave the proof as an exercise.

Example 14.9

Consider the interpretation where s _i (p)=T for even i and s _i (p)=F for odd i:

The formula □◊p is true, since for any i, σ _2i ⊨p. Obviously, ◊□p is false in all states of the diagram, because for any i, σ _i ⊨¬ p if i is odd and σ _i+1⊨¬ p if i is even. ■

Dual Theorems for ◊

We leave it as an exercise to prove the following theorems using the duality of □ and ◊ and the linearity of $\bigcirc$.

Theorem 14.10

$$ \begin{array}{*{20}l} {(a)} & { \vdash p \to \lozenge p} & {(b)} & { \vdash \bigcirc p \to \lozenge p} \\ {(c)} & { \vdash \square p \to \lozenge p} & {(d)} & { \vdash \square (p \to q) \to (\lozenge p \to \lozenge q)} \\ {(e)} & { \vdash \lozenge (p \vee q) \leftrightarrow (\lozenge p \vee \lozenge q)} & {(f)} & { \vdash \lozenge (p \wedge q) \to (\lozenge p \wedge \lozenge q)} \\ {(g)} & { \vdash \lozenge p \leftrightarrow p \vee \bigcirc \lozenge p} & {(h)} & { \vdash \lozenge \bigcirc p \leftrightarrow \bigcirc \lozenge p} \\ {(i)} & { \vdash \lozenge \lozenge p \leftrightarrow (p} & {} & {} \\ \end{array} $$

From Theorem 14.10(d), we obtain a generalization rule for ◊:

$$\displaystyle \frac{\vdash A \mathbin {\rightarrow }B}{\vdash \Diamond A \mathbin {\rightarrow }\Diamond B}.$$

Collapsing Sequences of Operators

The transitivity of □ (Theorem 14.6) and its dual for ◊ (Theorem 14.10(i)) show that any string of □’s or ◊’s can be collapsed. No expressive power is gained by using more than two operators in sequence, as shown by the following theorem.

Theorem 14.11

$$ \begin{array}{r@{\quad}l@{\qquad}r@{\quad}l} \textup{(a)}&\vdash \Box \Diamond \Box p \mathbin {\leftrightarrow }\Diamond \Box p& \textup{(b)}&\vdash \Diamond \Box \Diamond p\mathbin {\leftrightarrow }\Box \Diamond p. \end{array} $$

We prove (a) and then (b) follows by duality.

Proof

 ■

14.3 Soundness and Completeness of $L$ *

Soundness

Theorem 14.12

(Soundness of $L$)

Let A be a formula of LTL. If $\vdash _L A$ then ⊨A.

Proof

We need to show that each axiom is a valid LTL formula and that the two rules of inference preserve validity. By definition, valid formulas of propositional logic are valid, and the soundness of MP was shown in Theorem 3.37. The soundness of Axioms 1 and 5 was shown in Theorems 13.15 and 13.25, respectively. We leave the soundness of Axioms 2 and 3 as an exercise and show the soundness of the induction axiom and the generalization rule.

Axiom 4: :

$\vdash \square (A \to \bigcirc A) \to (A \to \square A)$.

If the formula is not valid, there exists an interpretation σ such that:

$$ \sigma \vDash \square (A \to \bigcirc A) \wedge A \wedge \neg \square A. $$

Since σ⊨A and σ⊨¬ □A there exists a smallest value i>0 such that σ _i ⊨¬ A and σ _j ⊨A for 0≤j<i. In particular, σ _i−1⊨A. But we also have that $\sigma \vDash \square (A \to \bigcirc A),$, so by definition of the □ operator, $\sigma _{i - 1} \vDash A \to \bigcirc A$. By MP we have $\sigma _{i - 1} \vDash \bigcirc A$ and thus σ _i ⊨A, contradicting σ _i ⊨¬ A.

Generalization: :

If ⊨A, then ⊨□A.

We need to show that for all interpretations σ, σ⊨□A. This means that for all i≥0, it is true that σ _i ⊨A. But ⊨A implies that for all interpretation σ′, σ′⊨A, in particular, this must hold for σ′=σ _i . ■

Completeness

Theorem 14.13

(Completeness of $L$)

Let A be a formula of LTL. If ⊨A then $\vdash _L A$.

Proof

If A is valid, the construction of a semantic tableau for ¬ A will fail, either because it closes or because all the MSCCs are non-fulfilling and were deleted. We show by induction that for every node in the tableau, the disjunction of the negations of the formulas labeling the node is provable in $L$. Since the formula labeling the root is ¬ A, it follows that ⊢¬ ¬ A, from which ⊢A follows by propositional logic.

The base case of the leaves and the inductive steps for the rules for α- and β-formulas follow by propositional reasoning together with the expansion axiom.

Suppose that the rule for an X-formula is used:

where we assume that negations are pushed inwards as justified by the linearity axiom. By the inductive hypothesis, ⊢¬ A ₁∨⋯∨¬ A _n . The following deduction proves the formula associated with the parent node:

There remains the case of a node that is part of a non-fulfilling MSCC. We demonstrate the technique on a specific example, proving $\vdash \square p \to \bigcirc \square p$ by constructing a semantic tableau for the negation of the formula.

The crucial part of the proof is to define the invariant of the loop, that is, a formula A such that $\vdash A \to \bigcirc A$. The invariant will be the conjunction of the formulas A _i , where $\bigcirc A_i$ are the next formulas in the states of the SCC, as these represent what must be true from one state to the next. In the example, for invariant is □p∧◊¬ p. We proceed to prove that this formula is inductive.

The leaf on the left of the tableau has a complementary pair of literals, so $\vdash \neg p \vee \neg \bigcirc \square p \vee \neg \neg p$ is an axiom. We use this formula together with formula (5) to prove the formula associated with l _β .

Line 14 is the disjunction of the complements of the formulas at node l _β . ■

The method used in the proof will almost certainly not yield the shortest possible proof of a formula, but it is an algorithmic procedure for discovering a proof of a valid LTL formula.

14.4 Axioms for the Binary Temporal Operators *

Section 13.6 presented several binary temporal operators, any one of which can be chosen as a basic operator and the others defined from it. If we choose $U$ as the basic operator, a complete axiom system is obtained by adding the following two axioms to the axioms of Definition 14.1:

$$ \begin{array}{*{20}l} {\mathbf{Axiom}\,\mathbf{6}} & {\mathbf{Expansion}\,\mathbf{of}\,{\text{U}}} & { - AUB \leftrightarrow (B \vee (A \wedge \bigcirc (AUB))).} \\ {\mathbf{Axiom}\,\mathbf{7}} & {\mathbf{Eventuality}} & { - AUB \to \Diamond B.} \\ \end{array} $$

$U$ is similar to ◊: Axiom 6 requires that either B is true today or A is true today and $AUB$ will be true tomorrow. Axiom 7 requires that B eventually be true.

14.5 Summary

The deductive system $L$ assumes that propositional reasoning can be informally applied. There are five axioms: the distributive and expansion axioms are straightforward, while the duality axiom for $\bigcirc$ is essential to capture the linearity of interpretations of LTL. The central axiom of $L$ is the induction axiom: since interpretations in LTL are infinite paths, proofs of non-trivial formulas usually require induction. The rules of inference are the familiar modus ponens and generalization using □. As usual, the proof of soundness is straightforward. Proving completeness is based on the existence of a non-fulfilling MSCC in a tableau. The formulas labeling the nodes of the MSCC can be used to construct a formula that can be proved by induction.

14.6 Further Reading

The deductive system $L$ and the proof of its soundness and completeness is based on Ben-Ari et al. (1983), although that paper used a different system of temporal logic. 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). Axioms for the various binary temporal operators are given in Kröger and Merz (2008, Chap. 3).

14.7 Exercises

14.1

Prove ⊢□(p∧q)→(□p∧□q) (Theorem 14.3).

14.2

Prove ⊢(□p∨□q)→□(p∨q) (Theorem 14.5) and show that the converse is not valid.

14.3

Prove the future formulas in Theorem 14.10.

14.4

Prove that Axioms 2 and 3 are valid.

14.5

Prove ⊢◊□◊p↔□◊p (Theorem 14.11) and ⊢◊□p→□◊p (Theorem 14.8).

14.6

Prove ⊢□(□◊p→◊q)↔(□◊q∨◊□¬ p).

14.7

Fill in the details of the proof of $\vdash \Box (\,(p\vee \Box q)\:\wedge\: (\Box p\vee q)\,) \;\mathbin {\leftrightarrow }\; (\Box p\vee \Box q)$.