Proving Possibility Properties

Leslie Lamport July 4, 1995

\begin{matrix}c \\ ◯ \end{matrix}Digital Equipment Corporation 1995

This work may not be copied or reproduced in whole or in part for any commercial purpose. Permission to copy in whole or in part without payment of fee is granted for nonprofit educational and research purposes provided that all such whole or partial copies include the following: a notice that such copying is by permission of the Systems Research Center of Digital Equipment Corporation in Palo Alto, California; an acknowledgment of the authors and individual contributors to the work; and all applicable portions of the copyright notice. Copying, reproducing, or republishing for any other purpose shall require a license with payment of fee to the Systems Research Center. All rights reserved.

Author’s Abstract

A method is described for proving “always possibly” properties of specifications in formalisms with linear-time trace semantics. It is shown to be relatively complete for TLA (Temporal Logic of Actions) specifications.

Contents

1 Introduction 1

2 Possibility and Closure 1 2.1 Closure and Safety . . . . . . . . . . . . . . . . . . . . . . . . 1 2.2 Possibility . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2

3 Proving Possibility Properties in TLA 3 3.1 TLA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 3.2 The Proof Method . . . . . . . . . . . . . . . . . . . . . . . . 5

4 Conclusion 7

Acknowledgments 7

References 8

Appendix 9 A.1 Proof of Proposition 2 . . . . . . . . . . . . . . . . . . . . . . 9 A.2 Proof of Proposition 3 . . . . . . . . . . . . . . . . . . . . . . 10 A.3 Proof of Proposition 4 . . . . . . . . . . . . . . . . . . . . . . 11 A.4 Proof of Proposition 5 . . . . . . . . . . . . . . . . . . . . . . 12

1 Introduction

Proving possibility properties provides no useful information about a system. Why prove that it is possible for a user to press q on the keyboard and for a q subsequently to appear on the screen? We know that the user can always press the q key, and what good is knowing that a q might appear on the screen? What we want to prove is that no q appears on the screen unless a q is typed (a safety property), and that, if a q is typed, then a q eventually does appear (a liveness property).

However, we do not reason about a system; we reason about a mathematical model of a system. A possibility property can provide a sanity check on our model. Proving that it is always possible for a press(q) action to occur tells us something useful about the model. In general, we want to prove that a model allows the occurrence of actions representing events that the system cannot prevent.

We present a method for proving that it is always possible for some state or action eventually to occur. This seems to be the most useful class of possibility properties. We first describe the general approach, which applies to any formalism with a linear-time semantics. We then show how the method is used with TLA, the Temporal Logic of Actions [8], and prove a relative completeness result.

Possibility properties pose no problem in formalisms based on branchingtime semantics [4]. However, it is impossible to assert in linear-time temporal logic that something is always possible [6]. It is therefore not obvious how to prove possibility properties in the formalisms that we consider, which are based on linear-time semantics.

2 Possibility and Closure

2.1 Closure and Safety

We begin by reviewing some basic concepts of linear-time temporal logic [10]. A behavior is an infinite sequence of states or of events—for now, it doesn’t matter which. The meaning [[Π]] of a temporal-logic formula Π is a Booleanvalued function on behaviors. We say that the behavior σ satisfies Π iff (if and only if) [[Π]](σ) equals true. Formula Π is valid, written ⊧ Π, iff every behavior satisfies Π. To use temporal logic to specify (a mathematical model of) a system, we consider states to represent possible system states and events to represent possible system actions, so a behavior represents a conceivable execution of a system. A system is specified by a formula Π that is satisfied by precisely those behaviors that represent a legal system execution.

Boolean operations on formulas are defined in the obvious way; for example, [[Π ∧ Φ]](σ) =^{Δ} [[Π]](σ) ∧ [[Φ]](σ). We define □Π to be the formula that is satisfied by a behavior σ iff every suffix of σ satisfies Π, and we define ◇Π to be satisfied by σ iff some suffix of σ satisfies Π. The operators □ and ◇ are read always and eventually, respectively. We define ⇝ by

Π ⇝ Φ =^{Δ} □(Π ⇒ ◇Φ).

Let S^{∞} be the set of all behaviors, let S^{∗} be the set of all finite behaviors (finite prefixes of elements of S^{∞}), let “·” be concatenation of sequences, and let ρ ⊏ σ mean that ρ is a finite prefix of the behavior σ. The closure C(Π) of a formula Π is defined by

[[C(Π)]](σ) =^{Δ} ∀ρ ⊏ σ : ∃τ ∈ S^{∞} : [[Π]](ρ · τ)  (1)

where ∀ρ ⊏ σ is universal quantification over all finite prefixes ρ of σ. Thus, a behavior σ satisfies C(Π) iff every finite prefix of σ can be extended to a behavior that satisfies Π. The following proposition follows easily from (1).

Proposition 1 For any formulas Π and Φ:

1. ⊧ Π ⇒ C(Π)

2. ⊧ Π ⇒ Φ implies ⊧ C(Π) ⇒ C(Φ)

A safety formula is one that equals its closure. Thus, a safety formula Π is satisfied by a behavior σ iff every prefix of σ can be extended to a behavior satisfying Π. Intuitively, a safety property Π constrains only the finite behavior of a system—any behavior that fails to satisfy Π fails at some specific instant. More precisely, Π is a safety property iff

∀σ ∈ S^{∞} : [[¬Π]](σ) ≡ ∃ρ ⊏ σ : ∀τ ∈ S^{∞} : [[¬Π]](ρ · τ)  (2)

2.2 Possibility

We now define a class of possibility properties and relate them to closure. The properties are of the form always possibly P, meaning that at all times during an execution of the system, it is possible for P eventually to become true. In linear-time temporal logic, it is impossible to write a formula whose meaning is always possibly P [6]. However, for any particular system, we can write a formula asserting that always possibly P holds for behaviors of that system. More precisely, we can define a formula P_{Π}(P) such that always possibly P holds for the system specified by Π iff P_{Π}(P) is valid.

Intuitively, always possibly P holds for a system iff, at any point during any execution of the system, it is possible to choose some particular way of continuing the execution that makes P eventually hold. In other words, if ρ is the prefix of a behavior satisfying the system’s specification Π, there exists a behavior τ such that ρ · τ satisfies Π, and P holds at some point in τ. We can therefore define P_{Π}(P) by

[[P_{Π}(P)]](σ) =^{Δ} [[Π]](σ) ⇒ ∀ρ ⊏ σ : ∃τ : [[Π]](ρ · τ) ∧ [[◇P]](τ) (3)

Our method of proving possibility properties is based on the following result. It and all subsequent propositions are proved in the appendix.

Proposition 2 If ¬P is a safety property, then

⊧ (C(Π) ⇒ C(C(Π) ∧ □◇P)) ⇒ P_{Π}(P)

We will use this result when [[P]](σ) depends only on the first one or two elements of σ. By (2), ¬P is a safety property for such a P.

3 Proving Possibility Properties in TLA

3.1 TLA

To apply Proposition 2, we need to compute closures. One can write TLA specifications in a way that makes computing the closure easy. We now give a thumbnail review of TLA; see [8] for a real explanation of the logic.

In TLA, behaviors are infinite sequences of states, where a state is an assignment of variables to values. We let S be the set of all states. Formulas are built from actions, Boolean operators, and the temporal operator □. An action is a Boolean expression containing primed and unprimed variables. For states s and t, we define [[A]](s, t) to equal true iff A holds with values from s substituted for unprimed variables and with values from t substituted for primed variables. We consider action A to be a temporal formula by letting [[A]](s_{0}, s_{1}, s_{2}, …) equal [[A]](s_{0}, s_{1}).

A state predicate P is an action with no primed variables; we write [[P]](s) instead of [[P]](s, t), which is independent of t. For an action A, we define the predicate Enabled A by [[Enabled A]](s) =^{Δ} ∃t ∈ S : [[A]](s, t). A state function is a nonBoolean expression containing unprimed variables. For any state function v, we let [A]_{v} =^{Δ} A ∨ (v′ = v) and ⟨A⟩_{v} =^{Δ} A ∧ (v′ ≠ v), where v′ is the expression obtained by priming the free variables in v.

The canonical form of a TLA formula is Init ∧ □[N ]_{v} ∧ F , where Init is a state predicate, N an action, v a state function, and F the conjunction of formulas of the form WF_{v}(A) or SF_{v}(A), with

WF_{v}(A) =^{Δ} □◇¬Enabled ⟨A⟩_{v} ∨ □◇⟨A⟩_{v}
SF_{v}(A) =^{Δ} ◇□¬Enabled ⟨A⟩_{v} ∨ □◇⟨A⟩_{v}

For example, a system that starts with x and y both 0, and repeatedly either increments x by ±1 or, if x equals 0, increments y by ±1, is specified by the following formula Πxy.^{1}

Nxy =^{Δ} ∨ \begin{matrix}∧ x′ ∈ \{x + 1, x − 1\} \\ ∧ y′ = y \end{matrix}

∨ \begin{matrix}∧ x = x′ = 0 \\ ∧ y′ ∈ \{y + 1, y − 1\} \end{matrix}

Πxy =^{Δ} (x = y = 0) ∧ □[Nxy]_{⟨x,y ⟩} ∧ WF_{⟨x,y ⟩}(Nxy)

The fairness condition WF_{⟨x,y ⟩}(Nxy) asserts that the system never stops.

TLA also has an operator ∃ ∃ ∃ ∃ ∃ ∃, where ∃ ∃ ∃ ∃ ∃ ∃ x : Π is essentially Π with variable x hidden. The system specified by ∃ ∃ ∃ ∃ ∃ ∃ x : Π satisfies a possibility property iff Π does, so we ignore the ∃ ∃ ∃ ∃ ∃ ∃ operator here. Using ∃ ∃ ∃ ∃ ∃ ∃, we can express P_{Π}(P) and C(Π) as TLA formulas, for any formulas Π and P. Propositions 1 and 2 can then be proved by temporal-logic reasoning.

Closures of TLA formulas are computed using the following result.

Proposition 3 If Init is a state predicate, M implies N , and F is the conjunction of countably many formulas of the form WF_{v}(A) and/or SF_{v}(A), where each ⟨A⟩_{v} implies M , then

C(Init ∧ □[N ]_{v} ∧ ◇□[M ]_{v} ∧ F ) ≡ Init ∧ □[N ]_{v}

Since □Π implies ◇□Π, for any Π, substituting Nxy for both N and M in the proposition proves that C(Πxy) ≡ (x = y = 0) ∧ □[Nxy]_{⟨x,y ⟩}. For M = N , Proposition 3 is a special case of Proposition 2 of [1].

A formula of the form Init ∧ □[N ]_{v} ∧ F is called machine closed [1] if its closure equals Init ∧ □[N ]_{v}. Proposition 3 implies that such a formula is machine closed if F is the conjunction of fairness conditions for actions that imply N . It can be argued that any specification that models a real implementation should be machine closed, and that possibility properties need be proved only for a model of an implementation, not for a high-level specification.

1A list of formulas bulleted with ∧ or ∨ denotes the conjunction or disjunction of the formulas; indentation is used to eliminate parentheses.

3.2 The Proof Method

We now show how to use Propositions 1, 2, and 3 to prove possibility properties of the form P_{Π}(P) for a state predicate P, where Π equals Init ∧ □[N ]_{v} ∧ F , and C(Π) equals Init ∧ □[N ]_{v}. For any action A, formula P_{Π}(A) is equivalent to P_{Π}(Enabled ([N ]_{v} ∧ A)). Hence, our method can be used to prove properties P_{Π}(A) for arbitrary actions A.

To prove P_{Π}(P), we find an action M and a conjunction G of fairness properties such that

Init ∧ □[N ]_{v} ∧ ◇□[M ]_{v} ∧ G ⇒ □◇P  (4)

and for which we can use Proposition 3 to prove

C(Init ∧ □[N ]_{v} ∧ ◇□[M ]_{v} ∧ G) ≡ Init ∧ □[N ]_{v}  (5)

We then deduce P_{Π}(P) as follows.

1. Init ∧ □[N ]_{v} ∧ ◇□[M ]_{v} ∧ G ⇒ Init ∧ □[N ]_{v} ∧ □◇P Proof: (4).

2. Init ∧ □[N ]_{v} ⇒ C(Init ∧ □[N ]_{v} ∧ □◇P)

Proof: (5) and part 2 of Proposition 1.

3. Q.E.D.

Proof: By Proposition 2, since Init ∧ □[N ]_{v} ≡ C(Π).

For example, to prove P_{Πxy} (y = 17), we take

M =^{Δ} ∨ ∧ ((x > 0) ∧ (x′ = x − 1)) ∨ ((x < 0) ∧ (x′ = x + 1)) ∧ y′ = y ∨ ∧ x = x′ = 0 ∧ ((y > 17) ∧ (y′ = y − 1)) ∨ ((y < 17) ∧ (y′ = y + 1))

To prove (4), we use the TLA rules from Figure 5 (page 888) of [8].

We now show that this proof method is complete relative to non-temporal reasoning about actions. This means that if all the necessary valid action formulas can be proved, then every valid formula P_{Π}(P) is provable. We write ⊢ Ψ to mean that formula Ψ is provable from Propositions 1, 2, and 3 and the rules in [8].

Our results assume only that valid actions in some class of expressible formulas are provable. We assume that expressible terms and formulas are closed under the operations of first-order logic (conjunction, quantification, etc.), priming, and forming tuples. Relative completeness results for programming logics are generally based on some form of predicate transformer analogous to the sin operator of [7]. For any action A and state predicate P, the state predicate sin(A, P) can be defined by

[[sin(A, P)]](s) =^{Δ}

∃s_{0}, …, s_{n} ∈ S : (s = s_{n}) ∧ [[P]](s_{0}) ∧ (∀i < n : [[A]](s_{i}, s_{i+1}))

(6)

for all states s. We first show completeness of the TLA rules for proving invariance properties.

Proposition 4 For any predicates I and Init, state function v, and action N , if

1. Every valid expressible action formula is provable.

2. I , Init, v, N , and sin([N ]_{v}, Init) are expressible.

3. ⊧ Init ∧ □[N ]_{v} ⇒ □I

then ⊢ Init ∧ □[N ]_{v} ⇒ □I .

Proposition 4 is essentially the TLA version of the classical completeness results for Hoare logics [3]. We use it to show completeness of our method for proving possibility properties:

Proposition 5 If

1. Every valid expressible action formula is provable.

2. P, Init, v, N , and sin([N ]_{v}, Init) are expressible.

3. ⊢ C(Π) ≡ Init ∧ □[N ]_{v}

4. ⊧ P_{Π}(P)

then ⊢ P_{Π}(P).

4 Conclusion

Proving possibility properties provides a way of checking that the mathematical models we make of our systems are sensible. For real time specifications, an important possibility property is nonZenoness, which asserts that it is always possible for time to advance. The relation between possibility and closure was first observed for nonZenoness in [1]. Our method generalizes a method described there for proving nonZenoness.

Propositions 1 and 2 are independent of TLA. They can be used for proving possibility properties in any trace-based specification method for which closures can be computed. It is easy to compute closures when specifications are written as certain kinds of transition systems. For example, the closure of (the temporal-logic formula corresponding to) a Büchi automaton [2] with a strongly connected state graph is the automaton obtained by making every state an accepting state. The closure of a specification written as a state transition system [5, 9] is obtained by removing the fairness properties, if those properties are expressed as fairness conditions on transitions. We do not know of any practical method for computing the closure of arbitrary temporal-logic formulas, or of transition systems with arbitrary temporal formulas as fairness requirements. We do not know how to prove possibility properties for traditional temporal-logic specifications [10].

Acknowledgments

Martín Abadi and Stephan Merz pointed out mistakes in the text of an earlier version. Fred Schneider suggested some improvements to the presentation.

References

[1] Martín Abadi and Leslie Lamport. An old-fashioned recipe for real time. ACM Transactions on Programming Languages and Systems, 16(5):1543–1571, September 1994.

[2] Bowen Alpern and Fred B. Schneider. Recognizing safety and liveness. Distributed Computing, 2(3):117–126, 1987.

[3] Krzysztof R. Apt. Ten years of Hoare’s logic: A survey—part one. ACM Transactions on Programming Languages and Systems, 3(4):431– 483, October 1981.

[4] E. Allen Emerson. Temporal and modal logic. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 16, pages 995–1072. Elsevier and MIT Press, Amsterdam and Cambridge, Massachusetts, 1990.

[5] Simon S. Lam and A. Udaya Shankar. Specifying modules to satisfy interfaces: A state transition system approach. Distributed Computing, 6(1):39–63, 1992.

[6] Leslie Lamport. ‘Sometime’ is sometimes ‘not never’: A tutorial on the temporal logic of programs. In Proceedings of the Seventh Annual Symposium on Principles of Programming Languages, pages 174–185. ACM SIGACT-SIGPLAN, January 1980.

[7] Leslie Lamport. win and sin: Predicate transformers for concurrency. ACM Transactions on Programming Languages and Systems, 12(3):396–428, July 1990.

[8] Leslie Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, May 1994.

[9] Nancy Lynch and Mark Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the Sixth Symposium on the Principles of Distributed Computing, pages 137–151. ACM, August 1987.

[10] Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, New York, 1991.

Appendix

We now prove Propositions 2–5. The proofs use a hierarchical style in which the proof of statement ⟨i⟩j is either an ordinary paragraph-style proof or the sequence of statements ⟨i+1⟩1, ⟨i+1⟩2, … and their proofs. We recommend reading proofs top-down—reading the proof of a level-k step by first reading the level-(k +1) statements that form the proof, together with the proof of the final Q.E.D. step, and then reading the proofs of the level-(k +1) steps in any order.

A.1 Proof of Proposition 2

To prove the proposition, we must prove that if a behavior σ satisfies C(Π) ⇒ C(C(Π) ∧ □◇P), then it satisfies P_{Π}(P). By the definition (3) of P_{Π}(P), the proposition is proved as follows. Assume: 1. [[Π]](σ)

2. [[C(Π) ⇒ C(C(Π) ∧ □◇P)]](σ)

Prove: ∀ρ ⊏ σ : ∃τ : [[Π]](ρ · τ) ∧ [[◇P]](τ) ⟨1⟩1. ∀ρ ⊏ σ : ∃η ∈ S^{∞} : [[C(Π)]](ρ · η) ∧ [[□◇P]](ρ · η)

⟨2⟩1. [[C(Π)(σ)]]

Proof: Assumption 1 and part 1 of Proposition 1. ⟨2⟩2. C(C(Π) ∧ □◇P)(σ)

Proof: ⟨2⟩1, assumption 2, and the definition of ⇒ for temporal formulas.

⟨2⟩3. Q.E.D.

Proof: ⟨2⟩2, (1), and the definition of ∧ for temporal formulas.

⟨1⟩2. ∀ρ ⊏ σ : ∃ξ ∈ S^{∗} : \begin{matrix}∧ ∃ϕ ∈ S^{∞} : [[Π]](ρ · ξ · ϕ) \\ ∧ ∀χ ∈ S^{∞} : [[◇P]](ξ · χ) \end{matrix}

⟨2⟩1. ∀ρ ∈ S^{∗}, η ∈ S^{∞} : [[□◇P]](ρ · η) ⇒ ∃η_{1}, η_{2} : η = η_{1} · η_{2} ∧ [[P]](η_{2})

Proof: By definition of □ and ◇. ⟨2⟩2. ∀η_{2} ∈ S^{∞} : [[P]](η_{2}) ⇒ ∃η_{3} ⊏ η_{2} : ∀χ ∈ S^{∞} : [[P]](η_{3} · χ)

Proof: By the hypothesis that ¬P is a safety property and (2) (substituting ¬P for Π).

⟨2⟩3. ∀ρ ∈ S^{∗}, η ∈ S^{∞} : [[□◇P]](ρ · η) ⇒ ∃ξ ⊏ η : ∀χ ∈ S^{∞} : [[◇P]](ξ · χ)

Proof: By ⟨2⟩1, ⟨2⟩2, and the definition of ◇, taking η_{1} · η_{3} for ξ. ⟨2⟩4. ∀ρ ∈ S^{∗}, η ∈ S^{∞}, ξ ⊏ η : [[C(Π)]](ρ · η) ⇒ ∃ϕ ∈ S^{∞} : [[Π]](ρ · ξ · ϕ)

Proof: By the definition (1) of C. ⟨2⟩5. Q.E.D.

Proof: ⟨1⟩1, ⟨2⟩3, and ⟨2⟩4.

⟨1⟩3. Q.E.D.

Proof: By ⟨1⟩2, letting τ be ξ · ϕ and substituting ϕ for χ.

A.2 Proof of Proposition 3

We prove the proposition for the special case that F consists of a single WF or SF formula, which is the only case used here. The general case is handled much as in the proof of Proposition 2 of [1]. In the following proof, W/SF denotes either WF or SF. Assume: 1. ⊧ M ⇒ N

2. ⊧ ⟨A⟩_{v} ⇒ M

3. σ ∈ S^{∞}

Prove: [[C(Init ∧ □[N ]_{v} ∧ ◇□[M ]_{v} ∧ W/SF_{v}(A))]](σ) ≡ [[Init ∧ □[N ]_{v}]](σ) ⟨1⟩1. Assume: ∀ρ ⊏ σ : ∃τ : [[Init ∧ □[N ]_{v} ∧ ◇□[M ]_{v} ∧ W/SF_{v}(A)]](ρ · τ)

Prove: [[Init ∧ □[N ]_{v}]](σ) Proof: Assumption ⟨1⟩ (from this step) implies that Init holds in the first state of σ and [N ]_{v} holds in every pair of successive states of σ, which implies [[Init ∧ □[N ]_{v}]](σ) by definition of □ and of [[B]] for an action B.

⟨1⟩2. Assume: 1. [[Init ∧ □[N ]_{v}]](σ)

2. ρ ⊏ σ

Prove: ∃τ : [[Init ∧ □[N ]_{v} ∧ ◇□[M ]_{v} ∧ W/SF_{v}(A)]](ρ · τ) ⟨2⟩1. Choose states s_{0}, s_{1}, … such that ρ = s_{0}, …, s_{n} and, for i ≥ n,

∧ [[Enabled ⟨A⟩_{v}]](s_{i}) ⇒ [[⟨A⟩_{v}]](s_{i}, s_{i+1})

∧ ¬[[Enabled ⟨A⟩_{v}]](s_{i}) ⇒ (s_{i+1} = s_{i})

Proof: The existence of the s_{i} follows from the definition of Enabled . ⟨2⟩2. [[□[M ]_{v}]](s_{n}, s_{n+1}, …)

⟨3⟩1. ∀i ≥ n : [[[M ]_{v}]](s_{i}, s_{i+1})

Proof: If [[Enabled ⟨A⟩_{v}]](s_{i}), this follows from assumption 2. If ¬[[Enabled ⟨A⟩_{v}]](s_{i}), this follows because [[[M ]_{v}]](s, s) holds for any state s. ⟨3⟩2. Q.E.D.

Proof: ⟨3⟩1 and the definitions of □ and of [[B]] for an action B. ⟨2⟩3. [[W/SF_{v}(A)]](s_{0}, s_{1}, …)

Proof: □◇Enabled ⟨A⟩_{v} implies [[Enabled ⟨A⟩_{v}]](s_{i}) for infinitely many i, which by ⟨2⟩1 implies [[⟨A⟩_{v}]](s_{i}, s_{i+1}) for infinitely many i, which implies [[□◇⟨A⟩_{v}]](s_{0}, s_{1}, …). The result then follows from the definition of WF and SF, since ¬□◇Enabled ⟨A⟩_{v} is equivalent to ◇□¬Enabled ⟨A⟩_{v}, which implies □◇¬Enabled ⟨A⟩_{v}.

⟨2⟩4. [[□[N ]_{v}]](s_{0}, s_{1}, …)

⟨3⟩1. ∀i : [[[N ]_{v}]](s_{i}, s_{i+1})

⟨4⟩1. Assume: i < n

Prove: [[[N ]_{v}]](s_{i}, s_{i+1}) Proof: ⟨2⟩1 and assumptions ⟨1⟩:1 and ⟨1⟩:2 (from step ⟨1⟩2).

⟨4⟩2. Assume: i ≥ n

Prove: [[[N ]_{v}]](s_{i}, s_{i+1}) Proof: By ⟨2⟩1 and, if [[Enabled ⟨A⟩_{v}]](s_{i}), then by assumptions 1 and 2, else by definition of [N ]_{v}.

⟨4⟩3. Q.E.D.

Proof: ⟨4⟩1 and ⟨4⟩2. ⟨3⟩2. Q.E.D.

Proof: ⟨3⟩1 and the definitions of □ and of [[B]] for an action B. ⟨2⟩5. Q.E.D.

Proof: ⟨2⟩2, ⟨2⟩3, ⟨2⟩4, the definition of [[Init]], and the definition of ◇, taking s_{n}, s_{n+1}, … for τ.

⟨1⟩3. Q.E.D.

Proof: ⟨1⟩1, ⟨1⟩2, and the definition (1) of C.

A.3 Proof of Proposition 4

⟨1⟩1. ⊢ Init ∧ □[N ]_{v} ⇒ □sin([N ]_{v}, Init)

⟨2⟩1. ⊧ Init ⇒ sin([N ]_{v}, Init)

Proof: Definition (6) of sin. ⟨2⟩2. ⊧ [N ]_{v} ∧ sin([N ]_{v}, Init) ⇒ sin([N ]_{v}, Init)′

Proof: Definition (6) of sin. ⟨2⟩3. ⊢ sin([N ]_{v}, Init) ∧ □[N ]_{v} ⇒ □sin([N ]_{v}, Init)

Proof: ⟨2⟩2, assumption 1, and proof rule INV1. ⟨2⟩4. Q.E.D.

Proof: ⟨2⟩1, ⟨2⟩3, and assumption 1. ⟨1⟩2. ⊢ sin([N ]_{v}, Init) ⇒ I

⟨2⟩1. ∀s ∈ S : [[sin([N ]_{v}, Init)]](s) ⇒ ∃s_{0}, …, s_{n} ∈ S : [[Init ∧ □[N ]_{v}]](s_{0}, …, s_{n}, s, s, s, …)

Proof: Definition (6) of sin, and the definitions of □ and [N ]_{v}. ⟨2⟩2. ∀s, s_{0}, …, s_{n} ∈ S : [[Init ∧ □[N ]_{v}]](s_{0}, …, s_{n}, s, s, s, …) ⇒ [[I ]](s)

Proof: Assumption 3 and definition of □I . ⟨2⟩3. ⊧ sin([N ]_{v}, Init) ⇒ I

Proof: ⟨2⟩1 and ⟨2⟩2. ⟨2⟩4. Q.E.D.

Proof: ⟨2⟩3 and assumption 1. ⟨1⟩3. Q.E.D.

Proof: ⟨1⟩1, ⟨1⟩2, and proof rule STL4 of [8].

A.4 Proof of Proposition 5

Let N be the set of natural numbers and let x_{1}, …, x_{n} be the free variables of P. Since [N ]_{v} ≡ [[N ]_{v}]_{⟨v,w ⟩}, by replacing N with [N ]_{v} and v with ⟨v, x_{1}, …, x_{n} ⟩, we can assume:

5. ⊧ (v′ = v) ⇒ (P′ = P)

In the following proof, P_{n} is the predicate that is true iff P can be made true by taking n N -steps, but with no fewer than n such steps. Let: P_{n} =^{Δ} if n = 0 then P else ∧ ∀i < n : ¬P_{i} ∧ Enabled (N ∧ (v′ ≠ v) ∧ P′_{n−1})

M =^{Δ} N ∧ (∀n : P_{n+1} ⇒ P′_{n}) ⟨1⟩1. ⊢ Init ∧ □[N ]_{v} ⇒ □(∃n : P_{n})

Let: π(s, n) =^{Δ} ∃s_{0}, …, s_{n} : ∧ (s = s_{0}) ∧ [[P]](s_{n}) ∧ ∀i < n : [[N ∧ (v′ ≠ v)]](s_{i}, s_{i+1})

⟨2⟩1. ∀(s_{0}, s_{1}, …) ∈ S^{∞} :

[[Init ∧ □[N ]_{v}]](s_{0}, s_{1}, …) ⇒ ∀i ∈ N : ∃n ∈ N : π(s_{i}, n) Proof: Assumptions 4 and 5 and the definition (3) of P_{Π}(P).

⟨2⟩2. ∀s ∈ S, n ∈ N : [[P_{n}]](s) ≡ π(s, n) ∧ (∀i < n : ¬π(s, i))

Proof: By induction on n from the definitions of P_{n}, π, and Enabled . ⟨2⟩3. ∀s ∈ S : [[∃n : P_{n}]](s) ≡ (∃n ∈ N : π(s, n))

Proof: ⟨2⟩2. ⟨2⟩4. ⊧ Init ∧ □[N ]_{v} ⇒ □(∃n : P_{n})

Proof: ⟨2⟩1, ⟨2⟩3, and the definitions of □ and [[[N ]_{v}]]. ⟨2⟩5. Q.E.D.

Proof: ⟨2⟩4, assumptions 2 and 1, and Proposition 4, since Enabled A is obtained by existential quantification over the primed variables of A, so it is expressible if A is, for any action A.

⟨1⟩2. Assume: k ∈ N

Prove: ⊢ □(∃n : P_{n}) ∧ □[M ]_{v} ∧ WF_{v}(M ) ⇒ (P_{k+1} ⇝ P_{k}) ⟨2⟩1. ⊢ P_{k+1} ∧ [M ]_{v} ⇒ P′_{k+1} ∨ P′_{k}

Proof: Definition of M and assumption 5. ⟨2⟩2. ⊢ P_{k+1} ∧ ⟨M ⟩_{v} ⇒ P′_{k}

Proof: Definition of M . ⟨2⟩3. ⊢ P_{k+1} ⇒ Enabled ⟨M ⟩_{v}

⟨3⟩1. ⊧ P_{k+1} ⇒ ∀n ≠ (k + 1) : ¬P_{n}

Proof: Definition of P_{n}. ⟨3⟩2. ⊧ P_{k+1} ⇒ (M ≡ N ∧ P′_{k})

Proof: ⟨3⟩1 and definition of M . ⟨3⟩3. ⊧ P_{k+1} ⇒ Enabled ⟨M ⟩_{v}

Proof: ⟨3⟩2 and the definition of P_{k+1}. ⟨3⟩4. Q.E.D.

Proof: ⟨3⟩3 and assumption 1. ⟨2⟩4. Q.E.D.

Proof: ⟨2⟩1–⟨2⟩3 and rule WF1 of [8]. ⟨1⟩3. ⊢ □(∃n : P_{n}) ∧ ◇□[M ]_{v} ∧ WF_{v}(M ) ⇒ □◇P

⟨2⟩1. ⊢ □(∃n : P_{n}) ∧ ◇□[M ]_{v} ∧ WF_{v}(M ) ⇒ ((∃n : P_{n}) ⇝ P)

Proof: ⟨1⟩2 and the Lattice Rule of [8]. ⟨2⟩2. ⊢ □F ∧ (F ⇝ G) ⇒ □◇G, for any temporal formulas F and G.

Proof: □F ∧ (F ⇝ G) ≡ □F ∧ □(F ⇒ ◇G) Definition of ⇝ ≡ □(F ∧ (F ⇒ ◇G)) Rule STL5 of [8]. ⇒ □◇G Rule STL4 of [8].

⟨2⟩3. Q.E.D.

Proof: ⟨2⟩1 and ⟨2⟩2. ⟨1⟩4. Q.E.D.

⟨2⟩1. ⊢ C(Init ∧ □[N ]_{v} ∧ ◇□[M ]_{v} ∧ WF_{v}(M )) ≡ Init ∧ □[N ]_{v}

Proof: Proposition 3, since ⊢ M ⇒ N by definition of M . ⟨2⟩2. ⊢ Init ∧ □[N ]_{v} ∧ ◇□[M ]_{v} ∧ WF_{v}(M ) ⇒ C(Π) ∧ □◇P

Proof: ⟨1⟩1, ⟨1⟩3, and assumption 3. ⟨2⟩3. ⊢ C(Π) ⇒ C(C(Π) ∧ □◇P)

Proof: ⟨2⟩1, ⟨2⟩2, assumption 3, and part 2 of Proposition 1. ⟨2⟩4. Q.E.D.

Proof: ⟨2⟩3 and Proposition 2.