An Old-Fashioned Recipe for Real Time

Martín Abadi and Leslie Lamport

Wed 22 Dec PST 1993 [17:32]

This is a revised version of SRC Research Report 91. It will appear in ACM Transactions on Programming Languages and Systems.

An Old-Fashioned Recipe for Real Time · i

Contents

1 Introduction 1

2 Closed Systems 2 2.1 The Lossy-Queue Example . . . . . . . . . . . . . . . . . . . . . . . 3 2.2 The Semantics of TLA . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.3 Safety and Fairness . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.4 History-Determined Variables . . . . . . . . . . . . . . . . . . . . . . 9

3 Real-Time Closed Systems 9 3.1 Time and Timers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 3.2 Reasoning About Time . . . . . . . . . . . . . . . . . . . . . . . . . . 13 3.3 The NonZeno Condition . . . . . . . . . . . . . . . . . . . . . . . . . 14 3.4 An Example: Fischer’s Protocol . . . . . . . . . . . . . . . . . . . . . 17

4 Open Systems 19 4.1 Receptiveness and Realizability . . . . . . . . . . . . . . . . . . . . . 19 4.2 The −▷ Operator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 4.3 Proving Machine Realizability . . . . . . . . . . . . . . . . . . . . . . 20 4.4 Reduction to Closed Systems . . . . . . . . . . . . . . . . . . . . . . 21 4.5 Composition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

5 Real-Time Open Systems 22 5.1 A Paradox . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 5.2 Timing Constraints in General . . . . . . . . . . . . . . . . . . . . . 25

6 Conclusion 26 6.1 What We Did . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 6.2 Beyond Real Time . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27

A Definitions A–1 A1 States and Behaviors . . . . . . . . . . . . . . . . . . . . . . . . . . . A–1 A2 Predicates and Actions . . . . . . . . . . . . . . . . . . . . . . . . . . A–1 A3 Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . A–2 A4 Closure and Safety . . . . . . . . . . . . . . . . . . . . . . . . . . . . A–2 A5 Realizability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . A–2

B Proofs A–3 B1 Proof Notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . A–3 B2 Proof of Proposition 2 . . . . . . . . . . . . . . . . . . . . . . . . . . A–3 B3 Proof of Proposition 3 . . . . . . . . . . . . . . . . . . . . . . . . . . A–4 B4 Two Lemmas About Machine-Realizability . . . . . . . . . . . . . . A–4 B5 Proof of Proposition 4 . . . . . . . . . . . . . . . . . . . . . . . . . . A–5 B6 Proof of Proposition 5 . . . . . . . . . . . . . . . . . . . . . . . . . . A–9 B7 Proof of Theorem 4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . A–10

B7.1 High-Level Proof of the Theorem . . . . . . . . . . . . . . . . A–11 B7.2 Detailed Proof of the Theorem . . . . . . . . . . . . . . . . . A–14

An Old-Fashioned Recipe for Real Time

MARTÍN ABADI and LESLIE LAMPORT Digital Equipment Corporation

Traditional methods for specifying and reasoning about concurrent systems work for real-time systems. Using TLA (the temporal logic of actions), we illustrate how they work with the examples of a queue and of a mutual-exclusion protocol. In general, two problems must be addressed: avoiding the real-time programming version of Zeno’s paradox, and coping with circularities when composing real-time assumption/guarantee specifications. Their solutions rest on properties of machine closure and realizability. Categories and Subject Descriptors: D.2.4 [Software Engineering]: Program Verification— correctness proofs; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs—Specification techniques General Terms: Theory, Verification Additional Key Words and Phrases: Composition, concurrent programming, liveness properties, real time, safety properties, temporal logic, Zeno

1. INTRODUCTION

A new class of systems is often viewed as an opportunity to invent a new semantics. A number of years ago, the new class was distributed systems. More recently, it has been real-time systems. The proliferation of new semantics may be fun for semanticists, but developing a practical method for reasoning formally about systems is a lot of work. It would be unfortunate if every new class of systems required inventing new semantics, along with proof rules, languages, and tools.

Fortunately, no fundamental change to the old methods for specifying and reasoning about systems is needed for these new classes. It has long been known that the methods originally developed for shared-memory multiprocessing apply equally well to distributed systems [Chandy and Misra 1988; Lamport 1982]. The first application we have seen of a clearly “off-the-shelf” method to a real-time algorithm was in 1983 [Neumann and Lamport 1983], but there were probably earlier ones. Indeed, the “extension” of an existing temporal logic to real-time programs by Bernstein and Harter [1981] can be viewed as an application of that logic.

The old-fashioned methods handle real time by introducing a variable, which we call now, to represent time. This idea is so simple and obvious that it seems hardly worth writing about, except that few people appear to be aware that it works in practice. We therefore describe how to apply a conventional method to real-time

Author’s address: Systems Research Center, Digital Equipment Corporation, 130 Lytton Avenue, Palo Alto, CA 94301. Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, the ACM copyright notice and the title of the publication and its date appear, and notice is given that copying is by permission of the Association for Computing Machinery. To copy otherwise, or to republish, requires a fee and/or specific permission.

\begin{matrix}c \\ ◯ \end{matrix} 1993 ACM 0000-0000/93/0000-0000 $00.00

ACM Transactions on Programming Languages and Systems, Vol ? No. ?, November 1993, Pages 1–A–21.

2 · Martín Abadi and Leslie Lamport

systems.

Any formalism for reasoning about concurrent programs can be used to prove properties of real-time systems. However, in a conventional formalism based on a programming language, real-time assumptions are expressed by adding program operations that read and modify the variable now. The result can be a complicated program that is hard to understand and easy to get wrong. We take as our formalism TLA, the temporal logic of actions [Lamport 1991]. In TLA, programs and properties are represented as logical formulas. A real-time program can be written as the conjunction of its untimed version, expressed in a standard way as a TLA formula, and its timing assumptions, expressed in terms of a few standard parameterized formulas. This separate specification of timing properties makes real-time specifications easier to write and understand.

The method is illustrated with two examples. The first is a queue in which the sender and receiver synchronize by the use of timing assumptions instead of acknowledgements. We indicate how safety and liveness properties of the queue can be proved. The second example is an n-process mutual exclusion protocol, in which mutual exclusion depends on assumptions about the length of time taken by the operations. Its correctness is proved by a conventional invariance argument.

We also discuss two problems that arise when time is represented as a program variable—problems that seem to have received little attention—and present new solutions.

The first problem is how to avoid the real-time programming version of Zeno’s paradox. If time becomes an ordinary program variable, then one can inadvertently write programs in which time behaves improperly. An obvious danger is deadlock, where time stops. A more insidious possibility is that time keeps advancing but is bounded, approaching closer and closer to some limit. One way to avoid such “Zeno” behaviors is to place an a priori lower bound on the duration of any action, but this can complicate the representation of some systems. We provide a more general and, we feel, a more natural solution.

The second problem is coping with the circularity that arises in open system specifications. The specification of an open system asserts that it operates correctly under some assumptions on the system’s environment. A modular specification method requires a rule asserting that, if each component satisfies its specification, then it behaves correctly in concert with other components. This rule is circular, because a component’s specification requires only that it behave correctly if its environment does, and its environment consists of all the other components. Despite its circularity, the rule is sound for specifications written in a particular style [Abadi and Lamport 1993; Misra and Chandy 1981; Pnueli 1984]. By examining an apparently paradoxical example, we discover how real-time specifications of open systems can be written in this style.

We express these problems and their solutions in terms of TLA. However, we believe that the problems will arise in any formalism that permits sufficiently general specifications. Our solutions should be applicable to any formalism whose semantics is based on sequences of states or actions.

2. CLOSED SYSTEMS

We briefly review how to represent closed systems in TLA. A closed system is one that is self-contained and does not communicate with an environment. No

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

An Old-Fashioned Recipe for Real Time · 3

one intentionally designs autistic systems; in a closed system, the environment is represented as part of the system. Open systems, in which the environment and system are separated, are discussed in Section 4.

We begin our review of TLA in Section 2.1 with an informal presentation of an example. The formal definitions are summarized in Section 2.2. A more leisurely exposition appears in [Lamport 1991], and most definitions in the current paper are repeated in a list in the appendix. Section 2.3 reviews the concepts of safety [Alpern and Schneider 1985] and machine closure [Abadi and Lamport 1991] (also known as feasibility [Apt, Francez, and Katz 1988]) and relates them to TLA, and Section 2.4 defines a useful class of history variables [Abadi and Lamport 1991]. Propositions and theorems are proved in the appendix.

2.1 The Lossy-Queue Example

We introduce TLA with the example of the lossy queue shown in Figure 1. The interface consists of two pairs of “wires”, each pair consisting of a val wire that holds a message and a boolean-valued bit wire. A message m is sent over a pair of wires by setting the val wire to m and complementing the bit wire. The receiver detects the presence of a new message by observing that the bit wire has changed value. Input to the queue arrives on the wire pair (ival, ibit), and output is sent on the wire pair (oval, obit). There is no acknowledgment protocol, so inputs are lost if they arrive faster than the queue processes them. (Because of the way ibit is used, inputs are lost in pairs.) The property guaranteed by this lossy queue is that the sequence of output messages is a subsequence of the sequence of input messages. In Section 3.1, we add timing constraints to rule out the possibility of lost messages.

A specification is a TLA formula Π describing a set of allowed behaviors. A property P is also a TLA formula. The specification Π satisfies property P iff (if and only if) every behavior allowed by Π is also allowed by P —that is, if Π implies P. Similarly, a specification Ψ implements Π iff every behavior allowed by Ψ is also allowed by Π, so implementation means implication.

The specification of the lossy queue is a TLA formula that mentions the four variables ibit, obit, ival, and oval, as well as two internal variables: q, which equals the sequence of messages received but not yet output; and last, which equals the value of ibit for the last received message. (The variable last is used to prevent the same message from being received twice.) These six variables are flexible variables; their values can change during a behavior. We also introduce a rigid variable Msg

[figure: ibit; ival; obit; oval; ^{q:  …}; last:]

Fig. 1. A simple queue.

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

Init_{Q}

=^{Δ} ∧ ibit, obit ∈ {true, false} ∧ ival, oval ∈ Msg ∧ last = ibit ∧ q = ⟨⟨⟩⟩

Inp =^{Δ}

∧ ibit′ = ¬ibit ∧ ival′ ∈ Msg ∧ (obit, oval, q, last)′ = (obit, oval, q, last)

EnQ =^{Δ}

∧ last ≠ ibit ∧ q′ = q ∘ ⟨⟨ival⟩⟩ ∧ last′ = ibit ∧ (ibit, obit, ival, oval)′ = (ibit, obit, ival, oval)

DeQ =^{Δ} ∧ q ≠ ⟨⟨⟩⟩

∧ oval′ = Head(q) ∧ q′ = Tail(q) ∧ obit′ = ¬obit ∧ (ibit, ival, last)′ = (ibit, ival, last)

N_{Q}  =^{Δ} Inp ∨ EnQ ∨ DeQ
v =^{Δ} (ibit, obit, ival, oval, q, last)
Π_{Q}  =^{Δ} Init_{Q} ∧ □[N_{Q}]_{v}
Φ_{Q}  =^{Δ} ∃ ∃ ∃ ∃ ∃ ∃q, last : Π_{Q}

Fig. 2. The TLA specification of a lossy queue.

denoting the set of possible messages; it has the same value throughout a behavior. We usually refer to flexible variables simply as variables, and to rigid variables as constants.

The TLA specification is shown in Figure 2, using the following notation. A list of formulas, each prefaced by ∧, denotes the conjunction of the formulas, and indentation is used to eliminate parentheses. The expression ⟨⟨ ⟩⟩ denotes the empty sequence, ⟨⟨m⟩⟩ denotes the singleton sequence having m as its one element, ∘ denotes concatenation, Head(σ) denotes the first element of σ, and Tail(σ) denotes the sequence obtained by removing the first element of σ. The symbol =^{Δ} means is defined to equal.

The first definition is of the predicate Init_{Q}, which describes the initial state. This predicate asserts that the values of variables ibit and obit are arbitrary booleans, the values of ival and oval are elements of Msg, the values of last and ibit are equal, and the value of q is the empty sequence.

Next is defined the action Inp, which describes all state changes that represent the sending of an input message. (Since this is the specification of a closed system, it includes the environment’s Inp action.) The first conjunct, ibit′ = ¬ibit, asserts that the new value of ibit equals the complement of its old value. The second conjunct asserts that the new value of ival is an element of Msg. The third conjunct asserts that the value of the four-tuple (obit, oval, q, last) is unchanged; it is equivalent to the assertion that the value of each of the four variables obit, oval, q, and last is unchanged. The action Inp is always enabled, meaning that, in any state, a new input message can be sent.

Action EnQ represents the receipt of a message by the system. The first conjunct

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

asserts that last is not equal to ibit, so the message on the input wire has not yet been received. The second conjunct asserts that the new value of q equals the sequence obtained by concatenating the old value of ival to the end of q’s old value. The third conjunct asserts that the new value of last equals the old value of ibit. The final conjunct asserts that the values of ibit, obit, ival, and oval are unchanged. Action EnQ is enabled in a state iff the values of last and ibit in that state are unequal.

The action DeQ represents the operation of removing a message from the head of q and sending it on the output wire. It is enabled iff the value of q is not the empty sequence.

The action N_{Q} is the specification’s next-state relation. It describes all allowed changes to the queue system’s variables. Since the only allowed changes are the ones described by the actions Inp, EnQ, and DeQ, action N_{Q} is the disjunction of those three actions.

In TLA specifications, it is convenient to give a name to the tuple of all relevant variables. Here, we call it v.

Formula Π_{Q} is the internal specification of the lossy queue—the formula specifying all sequences of values that may be assumed by the queue’s six variables, including the internal variables q and last. Its first conjunct asserts that Init_{Q} is true in the initial state. Its second conjunct, □[N_{Q}]_{v}, asserts that every step is either an N_{Q} step (a state change allowed by N_{Q}) or else leaves v unchanged, meaning that it leaves all six variables unchanged.

Formula Φ_{Q} is the actual specification, in which the internal variables q and last have been hidden. A behavior satisfies Φ_{Q} iff there is some way to assign sequences of values to q and last such that Π_{Q} is satisfied. The free variables of Φ_{Q} are ibit, obit, ival, and oval, so Φ_{Q} specifies what sequences of values these four variables can assume. All the preceding definitions just represent one possible way of structuring the definition of Φ_{Q}; there are infinitely many ways to write formulas that are equivalent to Φ_{Q} and are therefore equivalent specifications.

TLA is an untyped logic; variables may assume any values in a fixed universal domain. Type correctness can be expressed by the formula □T, where T is the predicate asserting that all relevant variables have values of the expected “types”. For the internal queue specification, the type-correctness predicate is

T_{Q} =^{Δ} ∧ ibit, obit, last ∈ {true, false} ∧ ival, oval ∈ Msg ∧ q ∈ Msg^{∗}  (1)

where Msg^{∗} is the set of finite sequences of messages. Type correctness of Π_{Q} is asserted by the formula Π_{Q} ⇒ □T_{Q}, which is easily proved [Lamport 1991]. Type correctness of Φ_{Q} follows from Π_{Q} ⇒ □T_{Q} by the usual rules for reasoning about quantifiers.

Formulas Π_{Q} and Φ_{Q} are safety properties, meaning that they are satisfied by an infinite behavior iff they are satisfied by every finite initial portion of the behavior. Safety properties allow behaviors in which a system performs properly for a while and then the values of all variables are frozen, never to change again. In asynchronous systems, such undesirable behaviors are ruled out by adding fairness properties. We could strengthen our lossy-queue specification by conjoining the weak fairness property WF_{v}(DeQ) and the strong fairness property SF_{v}(EnQ) to

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

Π_{Q}, obtaining

∃ ∃ ∃ ∃ ∃ ∃ q, last : (Init_{Q} ∧ □[N_{Q}]_{v} ∧ WF_{v}(DeQ) ∧ SF_{v}(EnQ))  (2)

Property WF_{v}(DeQ) asserts that if action DeQ is enabled forever, then infinitely many DeQ steps must occur. This property implies that every message reaching the queue is eventually output. Property SF_{v}(EnQ) asserts that if action EnQ is enabled infinitely often, then infinitely many EnQ steps must occur. It implies that if infinitely many inputs are sent, then the queue must receive infinitely many of them. The formula (2) implies the liveness property [Alpern and Schneider 1985] that an infinite number of inputs produces an infinite number of outputs. A formula such as (2), which is the conjunction of an initial predicate, a term of the form □[A]_{f}, and a fairness property, is said to be in canonical form.

2.2 The Semantics of TLA

We begin with some definitions. We assume a universal domain of values, and we let [[F]] denote the semantic meaning of a formula F.

state. A mapping from variables to values. We let s.x denote the value that state s assigns to variable x.

state function. An expression formed from variables, constants, and operators. The meaning of a state function is a mapping from states to values. For example, x + 1 is a state function such that [[x + 1]](s) equals s.x + 1, for any state s.

predicate. A boolean-valued state function, such as x > y + 1.

transition function. An expression formed from variables, primed variables, constants, and operators. The meaning of a transition function is a mapping from pairs of states to values, with unprimed variables referring to the first state of a pair and primed variables to the second. For example, x + y′ + 1 is a transition function, and [[x + y′ + 1]](s, t) equals the value s.x + t.y + 1, for any pair of states s, t.

action. A boolean-valued transition function, such as x > (y′ + 1).

step. A pair of states s, t. For an action A, the pair is called an A step iff [[A]](s, t) equals true. It is called a stuttering step iff s = t.

f′. The transition function obtained from the state function f by priming all the free variables of f, so [[f′]](s, t) = [[f]](t) for any states s and t.

[A]_{f}. The action A ∨ (f′ = f), for any action A and state function f.

⟨A⟩_{f}. The action A ∧ (f′ ≠ f), for any action A and state function f.

Enabled A. For any action A, the predicate such that [[Enabled A]](s) equals ∃t : [[A]](s, t), for any state s.

Informally, we often identify a formula and its meaning. For example we say that a predicate P is true in state s instead of [[P]](s) = true.

An RTLA (raw TLA) formula is a boolean expression built from actions, classical operators (boolean operators and quantification over rigid variables), and the unary temporal operator □. The meaning of an RTLA formula is a boolean-valued function on behaviors, where a behavior is an infinite sequence of states. The meaning of the operator □ is defined by

[[□F]](s_{1}, s_{2}, s_{3}, …) =^{Δ} ∀ n > 0 : [[F]](s_{n}, s_{n+1}, s_{n+2}, …)

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

Intuitively, □F asserts that F is always true. The meaning of an action as an RTLA formula is defined in terms of its meaning as an action by letting [[A]](s_{1}, s_{2}, s_{3}, …) equal [[A]](s_{1}, s_{2}). A predicate P is an action; P is true for a behavior iff it is true for the first state of the behavior, and □P is true iff P is true in all states. For any action A and state function f, the formula □[A]_{f} is true for a behavior iff each step is an A step or else leaves f unchanged. The classical operators have their usual meanings.

A TLA formula is one that can be constructed from predicates and formulas □[A]_{f} using classical operators, □, and existential quantification over flexible variables. Thus, an action that is not a predicate can appear in a TLA formula F only as a subformula of an action A in a subformula □[A]_{f} or Enabled A of F. The semantics of actions, classical operators, and □ are defined as before. The approximate meaning of quantification over a flexible variable is that ∃ ∃ ∃ ∃ ∃ ∃x : F is true for a behavior iff there is some sequence of values that can be assigned to x that makes F true. The precise definition appears in [Lamport 1991] and is recalled in the appendix. As usual, we write ∃ ∃ ∃ ∃ ∃ ∃ x_{1}, …, x_{n} : F instead of ∃ ∃ ∃ ∃ ∃ ∃ x_{1} : … ∃ ∃ ∃ ∃ ∃ ∃ x_{n} : F.

A property is a set of behaviors that is invariant under stuttering, meaning that it contains a behavior σ iff it contains every behavior obtained from σ by adding and/or removing stuttering steps. The set of all behaviors satisfying a TLA formula is a property, which we often identify with the formula.

For any TLA formula F, action A, and state function f:

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

These are TLA formulas, since ◇⟨A⟩_{f} equals ¬□[¬A]_{f}.

2.3 Safety and Fairness

A finite behavior is a finite sequence of states. We say that a finite behavior satisfies a property F iff it can be continued to an infinite behavior in F. A property F is a safety property [Alpern and Schneider 1985] iff the following condition holds: F contains a behavior iff it is satisfied by every finite prefix of the behavior.^{1} Intuitively, a safety property asserts that something “bad” does not happen. Predicates and formulas of the form □[A]_{f} are safety properties.

Safety properties are closed sets in a topology on the set of all behaviors [Abadi and Lamport 1991]. Hence, if two TLA formulas F and G are safety properties, then F ∧ G is also a safety property. The closure C(F) of a property F is the smallest safety property containing F. It can be shown that C(F) is expressible in TLA, for any TLA formula F.

If Π is a safety property and L an arbitrary property, then the pair (Π, L) is machine closed iff every finite behavior satisfying Π can be extended to an infinite behavior in Π ∧ L. Two equivalent definitions are that (Π, L) is machine closed iff (i) C(Π ∧ L) equals Π, or (ii) for any safety property Ψ, if Π ∧ L implies Ψ then Π implies Ψ. The lack of machine closure can be a source of incompleteness for proof

1One sometimes defines s_{1}, …, s_{n} to satisfy F iff the behavior s_{1}, …, s_{n}, s_{n}, s_{n}, … is in F. Since properties are invariant under stuttering, this alternative definition leads to the same definition of a safety property.

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

methods. Most methods for proving safety properties use only safety properties as hypotheses, so they can prove Π ∧ L ⇒ Ψ for safety properties Π and Ψ only by proving Π ⇒ Ψ. If Π is not machine closed, then Π∧L ⇒ Ψ could hold even though Π ⇒ Ψ does not, and these methods will be unable to prove that the system with specification Π satisfies Ψ.

Proposition 1 below shows that machine closure generalizes the concept of fairness. The canonical form for a TLA formula is

∃ ∃ ∃ ∃ ∃ ∃ x : (Init ∧ □[N]_{v} ∧ L)  (3)

where Init is a predicate, N is an action, v is a state function, L is a formula, (Init ∧ □[N]_{v}, L) is machine closed, and x is a tuple of variables called the internal variables of the formula. Usually, v will be the tuple of all variables appearing free in Init, N, and L (including the variables of x). It follows from the definitions that a behavior satisfies (3) iff there is some way of choosing values for x such that (a) Init is true in the initial state, (b) every step is either an N step or leaves all the variables in v unchanged, and (c) the entire behavior satisfies L.

An action A is said to be a subaction of a safety property Π iff, whenever an A step is possible, an A step that satisfies Π is possible. More precisely, A is a subaction of Π iff for every finite behavior s_{1}, …, s_{n} satisfying Π with Enabled A true in state s_{n}, there exists a state s_{n+1} such that (s_{n}, s_{n+1}) is an A step and s_{1}, …, s_{n+1} satisfies Π. By this definition, if A implies N then A is a subaction of Init ∧ □[N]_{v}. The exact condition is that A is a subaction of Init ∧ □[N]_{v} iff^{2}

Init ∧ □[N]_{v} ⇒ □((Enabled A) ⇒ Enabled (A ∧ [N]_{v}))

Two actions are disjoint iff their conjunction is identically false. A weaker notion is disjointness of two actions for a property: A and B are disjoint for Π iff no behavior satisfying Π contains an A ∧ B step. By this definition, A and B are disjoint for Init ∧ □[N]_{v} iff

Init ∧ □[N]_{v} ⇒ □¬Enabled (A ∧ B ∧ [N]_{v})

The following result shows that the conjunction of WF and SF formulas is a fairness property. It is a special case of Proposition 4 of Section 4.

Proposition 1. If Π is a safety property and L is the conjunction of a finite or countably infinite number of formulas of the form WF_{w}(A) and/or SF_{w}(A) such that each ⟨A⟩_{w} is a subaction of Π, then (Π, L) is machine closed.

In practice, each w will usually be a tuple of variables changed by the corresponding action A, so ⟨A⟩_{w} will equal A.^{3} In the informal exposition, we often omit the subscript and talk about A when we really mean ⟨A⟩_{w}.

Machine closure for more general classes of properties can be proved with the following two propositions, which are proved in the appendix. To apply the first, one must prove that ∃ ∃ ∃ ∃ ∃ ∃x : Π is a safety property. By Proposition 2 of [Abadi and Lamport 1991, page 265], it suffices to prove that Π has finite internal nondeterminism (fin), with x as its internal state component. Here, fin means roughly that there are only a finite number of sequences of values for x that can make a finite behavior satisfy Π.

2We let ⇒ have lower precedence than the other boolean operators. 3More precisely, T ∧ A will imply w′ ≠ w, where T is the type-correctness invariant.

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

Proposition 2. If (Π, L) is machine closed, x is a tuple of variables that do not occur free in L, and ∃ ∃ ∃ ∃ ∃ ∃x : Π is a safety property, then ((∃ ∃ ∃ ∃ ∃ ∃x : Π), L) is machine closed.

Proposition 3. If (Π, L_{1}) is machine closed and Π ∧ L_{1} implies L_{2}, then (Π, L_{2}) is machine closed.

2.4 History-Determined Variables

A history-determined variable is one whose current value can be inferred from the current and past values of other variables. For the precise definition, let

Hist(h, f, g, v) =^{Δ} (h = f) ∧ □[(h′ = g) ∧ (v′ ≠ v)]_{(h,v)}  (4)

where f and v are state functions and g is a transition function. A variable h is a history-determined variable for a formula Π iff Π implies Hist(h, f, g, v), for some f, g, and v such that h occurs free in neither f nor v, and h′ does not occur free in g.

If f and v do not depend on h, and g does not depend on h′, then ∃ ∃ ∃ ∃ ∃ ∃h : Hist(h, f, g, v) is true for all behaviors. Therefore, if h does not occur free in formula Φ, then ∃ ∃ ∃ ∃ ∃ ∃h : (Φ ∧ Hist(h, f, g, v)) is equivalent to Φ. In other words, conjoining Hist(h, f, g, v) to Φ does not change the behavior of its variables, so it makes h a “dummy variable” for Φ—in fact, it is a special kind of history variable [Abadi and Lamport 1991, page 270].

As an example, we add to the lossy queue’s specification Φ_{Q} a history variable hin that records the sequence of values transmitted on the input wire. Let

H_{in} =^{Δ} ∧ hin = ⟨⟨ ⟩⟩ ∧ □[ \begin{matrix}∧ hin′ = hin ∘ ⟨⟨ival′⟩⟩ \\ ∧ (ival, ibit)′ ≠ (ival, ibit) ]_{(hin,ival,ibit)} \end{matrix}  (5)

Then H_{in} equals Hist(hin, ⟨⟨ ⟩⟩, hin ∘ ⟨⟨ival′⟩⟩, (ival, ibit)); therefore, hin is a historydetermined variable for Φ_{Q} ∧ H_{in}, and ∃ ∃ ∃ ∃ ∃ ∃ hin : (Φ_{Q} ∧ H_{in}) equals Φ_{Q}.

If h is a history-determined variable for a property Π, then Π is fin, with h as its internal state component. Hence, if Π is a safety property, then ∃ ∃ ∃ ∃ ∃ ∃h : Π is also a safety property.

3. REAL-TIME CLOSED SYSTEMS

We now use TLA to specify and reason about timing properties of closed systems. We focus on worst-case upper and lower bounds on real-time delays. However, our approach should be applicable to other real-time properties as well. We believe that its only inherent limitation is that it cannot handle probabilistic real-time properties, such as average delay requirements. This limitation arises because, like most specification formalisms, TLA cannot express probabilistic properties.

Section 3.1 explains how time and timing properties can be represented with TLA formulas, and Section 3.2 describes how to reason about these formulas. The problem of Zeno specifications is addressed in Section 3.3. Our method of specifying and reasoning about timing properties is illustrated in Section 3.4 with the example of a real-time mutual exclusion protocol.

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

3.1 Time and Timers

In real-time TLA specifications, real time is represented by the variable now. Although it has a special interpretation, now is just an ordinary variable of the logic. The value of now is always a real number, and it never decreases—conditions expressed by the TLA formula

RT =^{Δ} (now ∈ R) ∧ □[now′ ∈ ((now, ∞))]_{now}

where R is the set of real numbers and ((r, ∞)) is {t ∈ R : t > r}.

It is convenient to make time-advancing steps distinct from ordinary program steps. This is done by strengthening the formula RT to

RT_{v} =^{Δ} (now ∈ R) ∧ □[(now′ ∈ ((now, ∞))) ∧ (v′ = v)]_{now}

This property differs from RT only in asserting that v does not change when now advances. Simple logical manipulation shows that RT_{v} is equivalent to RT ∧□[now′ = now]_{v}, and

Init ∧ □[N]_{v} ∧ RT_{v} = Init ∧ □[N ∧ (now′ = now)]_{v} ∧ RT

We express real-time constraints by placing timing bounds on actions. Such bounds are the bread-and-butter of many real-time formalisms, such as real-time process algebras [de Bakker, Huizing, de Roever, and Rozenberg 1992]. Timing bounds on actions are imposed by using timers to restrict the increase of now. A timer for Π is a state function t such that Π implies □(t ∈ R ∪ {±∞}). Timer t is used as an upper-bound timer by conjoining the formula

MaxTime(t) =^{Δ} (now ≤ t) ∧ □[now′ ≤ t′]_{now}

to a specification. This formula asserts that now is never advanced past t. Timer t is used as a lower-bound timer for an action A by conjoining the formula

MinTime(t, A, v) =^{Δ} □[A ⇒ (t ≤ now)]_{v}

to a specification. This formula asserts that an ⟨A⟩_{v} step cannot occur when now is less than t.^{4}

A common type of timing constraint asserts that an A step must occur within δ seconds of when the action A becomes enabled, for some constant δ. After an A step, the next A step must occur within δ seconds of when action A is re-enabled. There are at least two reasonable interpretations of this requirement.

The first interpretation is that the A step must occur if A has been continuously enabled for δ seconds. This is expressed by MaxTime(t) when t is a state function

4Unlike the usual timers in computer systems that represent an increment of time, our timers represent an absolute time. To allow the type of strict time bound that would be expressed by replacing ≤ with < in the definition of MaxTime or MinTime, we could introduce, as additional possible values for timers, the set of all “infinitesimally shifted” real numbers r^{−}, where t ≤ r^{−} iff t < r, for any reals t and r.

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

satisfying

VTimer(t, A, δ, v) =^{Δ} ∧ t = if Enabled ⟨A⟩_{v} then now + δ else ∞ ∧ □[ \begin{matrix}∧ t′ = if (Enabled ⟨A⟩_{v})′ then if ⟨A⟩_{v} ∨ ¬Enabled ⟨A⟩_{v} then now + δ else t else ∞ \\ ∧ v′ ≠ v ]_{(t,v)} \end{matrix}

Such a t is called a volatile δ-timer.

Another interpretation of the timing requirement is that an A step must occur if A has been enabled for a total of δ seconds, though not necessarily continuously enabled. This is expressed by MaxTime(t) when t satisfies

PTimer(t, A, δ, v) =^{Δ} ∧ t = now + δ ∧ □[ \begin{matrix}∧ t′ = if Enabled ⟨A⟩_{v} then if ⟨A⟩_{v} then now + δ else t else t + (now′ − now) \\ ∧ (v, now)′ ≠ (v, now) ]_{(t,v,now)} \end{matrix}

Such a t is called a persistent δ-timer. We can use δ-timers as lower-bound timers as well as upper-bound timers.

Observe that VTimer(t, A, δ, v) has the form Hist(t, f, g, v) and PTimer(t, A, δ, v) has the form Hist(t, f, g, (v, now)), where Hist is defined by (4). Thus, if formula Π implies that a variable t satisfies either of these formulas, then t is a historydetermined variable for Π.

As an example of the use of timers, we make the lossy queue of Section 2.1 nonlossy by adding the following timing constraints.

—Values must be put on a wire at most once every δ_{snd} seconds. There are two conditions—one on the input wire and one on the output wire. They are expressed by using δ_{snd}-timers t_{Inp} and t_{DeQ}, for the actions Inp and DeQ, as lower-bound timers.

—A value must be added to the queue at most Δ_{rcv} seconds after it appears on the input wire. This is expressed by using a Δ_{rcv}-timer T_{EnQ}, for the enqueue action, as an upper-bound timer.

—A value must be sent on the output wire within Δ_{snd} seconds of when it reaches the head of the queue. This is expressed by using a Δ_{snd}-timer T_{DeQ}, for the dequeue action, as an upper-bound timer.

The timed queue will be nonlossy if Δ_{rcv} < δ_{snd}. In this case, we expect the Inp, EnQ, and DeQ actions to remain enabled until they are “executed”, so it doesn’t matter whether we use volatile or persistent timers. We use volatile timers because they are a little easier to reason about.

The timed version Π_{Q}^{t} of the queue’s internal specification Π_{Q} is obtained by

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

Init_{Q}^{t}

=^{Δ} ∧ Init_{Q} ∧ now ∈ R ∧ t_{Inp} = now + δ_{snd} ∧ t_{DeQ} = T_{EnQ} = T_{DeQ} = ∞

Inp^{t} =^{Δ} ∧ Inp

∧ t_{Inp} ≤ now ∧ tInp^{′} = now′ + δ_{snd} ∧ TEnQ^{′} = if last′ ≠ ibit′ then now′ + Δ_{rcv} else ∞ ∧ (t_{DeQ} , T_{DeQ} )′ = if q = ⟨⟨ ⟩⟩ then (∞, ∞) else (t_{DeQ} , T_{DeQ} ) ∧ now′ = now

EnQ^{t} =^{Δ} ∧ EnQ

∧ TEnQ^{′} = ∞

∧ (t_{DeQ} , T_{DeQ} )′ = if q = ⟨⟨ ⟩⟩ then (now + δ_{snd} , now + Δ_{snd} ) else (t_{DeQ} , T_{DeQ} )

∧ (t_{Inp}, now)′ = (t_{Inp}, now)

DeQ^{t} =^{Δ} ∧ DeQ

∧ t_{DeQ} ≤ now ∧ (t_{DeQ} , T_{DeQ} )′ = if q′ = ⟨⟨ ⟩⟩ then (∞, ∞) else (now + δ_{snd} , now + Δ_{snd} )

∧ TEnQ^{′} = if last′ = ibit′ then ∞ else T_{EnQ} ∧ (t_{Inp}, now)′ = (t_{Inp}, now)

QTick =^{Δ}

∧ now′ ∈ ((now, min(T_{DeQ} , T_{EnQ} )]] ∧ (v, t_{Inp}, t_{DeQ} , T_{DeQ} , T_{EnQ} )′ = (v, t_{Inp}, t_{DeQ} , T_{DeQ} , T_{EnQ} )

vt =^{Δ} (v, now, t_{Inp}, t_{DeQ} , T_{DeQ} , T_{EnQ} )

Π_{Q}^{t} =^{Δ} ∧ Init_{Q}^{t}

∧ □[Inp^{t} ∨ EnQ^{t} ∨ DeQ^{t} ∨ QTick]_{vt}

Fig. 3. The canonical form for Π_{Q}^{t}, where ((r, s]] denotes the set of reals u such that r < u ≤ s.

conjoining the timing constraints to Π_{Q}:

Π_{Q}^{t} =^{Δ} ∧ Π_{Q} ∧ RT_{v} ∧ VTimer(t_{Inp}, Inp, δ_{snd}, v) ∧ MinTime(t_{Inp}, Inp, v) ∧ VTimer(t_{DeQ}, DeQ, δ_{snd}, v) ∧ MinTime(t_{DeQ}, DeQ, v) ∧ VTimer(T_{EnQ}, EnQ, Δ_{rcv}, v) ∧ MaxTime(T_{EnQ}) ∧ VTimer(T_{DeQ}, DeQ, Δ_{snd}, v) ∧ MaxTime(T_{DeQ})  (6)

The external specification Φ_{Q}^{t} of the timed queue is obtained by existentially quantifying first the timers and then the variables q and last.

Formula Π_{Q}^{t} of (6) is not in the canonical form for a TLA formula. A straightforward calculation, using the type-correctness invariant (1) and the equivalence of (□F) ∧ (□G) and □(F ∧ G), converts the expression (6) for Π_{Q}^{t} to the canonical form given in Figure 3.^{5} Observe how each subaction A of the original formula has a corresponding timed version A^{t}. Action A^{t} is obtained by conjoining A with the appropriate relations between the old and new values of the timers. If A has

5Further simplification of this formula is possible, but it requires an invariant. In particular, the fourth conjunct of DeQ^{t} can be replaced by TEnQ^{′} = T_{EnQ} .

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

a lower-bound timer, then A^{t} also has a conjunct asserting that it is not enabled when now is less than this timer. (The lower-bound timer t_{Inp} for Inp does not affect the enabling of other subactions because Inp is disjoint from all other subactions; a similar remark applies to the lower-bound timer t_{DeQ}.) There is also a new action, QTick, that advances now.

Formula Π_{Q}^{t} is the TLA specification of a program that satisfies each maximumdelay constraint by preventing now from advancing before the constraint has been satisfied. Thus, the program “implements” timing constraints by stopping time, an apparent absurdity. However, the absurdity results from thinking of a TLA formula, or the abstract program that it represents, as a prescription of how something is accomplished. A TLA formula is really a description of what is supposed to happen. Formula Π_{Q}^{t} says only that an action occurs before now reaches a certain value. It is just our familiarity with ordinary programs that makes us jump to the conclusion that now is being changed by the system.

3.2 Reasoning About Time

Formula Π_{Q}^{t} is a safety property; it is satisfied by a behavior in which no variables change values. In particular, it allows behaviors in which time stops. We can rule out such behaviors by conjoining to Π_{Q}^{t} the liveness property

NZ =^{Δ} ∀ t ∈ R : ◇(now > t)

which asserts that now gets arbitrarily large. However, when reasoning only about real-time (safety) properties, this should not be necessary. For example, suppose we want to show that our timed queue satisfies a real-time property expressed by formula Ψ^{t}, which is also a safety property. If Π_{Q}^{t} implies Ψ^{t}, then Π_{Q}^{t} ∧NZ implies Ψ^{t} ∧ NZ . Conversely, we don’t expect conjoining a liveness property to add safety properties; if Π_{Q}^{t} ∧ NZ implies Ψ^{t}, then Π_{Q}^{t} by itself should imply Ψ^{t}. Hence, there should be no need to introduce the liveness property NZ . Section 3.3 below explains precisely when we can ignore property NZ .

A safety property we might want to prove for the timed queue is that it does not lose any inputs. To express this property, let hin be the history variable, determined by H_{in} of (5), that records the sequence of input values; and let hout and H_{out} be the analogous history variable and property for the outputs. The assertion that the timed queue loses no inputs is expressed by

Π_{Q}^{t} ∧ H_{in} ∧ H_{out} ⇒ □(hout ⪯ hinp)

where α ⪯ β iff α is an initial prefix of β. This is a standard invariance property. The usual method for proving such properties leads to the following invariant

∧ T_{Q} ∧ (t_{Inp}, now ∈ R) ∧ (T_{EnQ}, t_{DeQ}, T_{DeQ} ∈ R ∪ {∞})
∧ now ≤ min(T_{EnQ}, T_{DeQ})
∧ (last = ibit) ⇒ (T_{EnQ} = ∞) ∧ (hinp = hout ∘ q)
∧ (last ≠ ibit) ⇒ (T_{EnQ} < t_{Inp}) ∧ (hinp = hout ∘ q ∘ ⟨⟨ival⟩⟩)
∧ (q = ⟨⟨ ⟩⟩) ≡ (T_{DeQ} = ∞)

and to the necessary assumption Δ_{rcv} < δ_{snd}. (Recall that T_{Q} is the typecorrectness predicate (1) for Π_{Q}.) Property NZ is not needed to prove this invariant.

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

Property NZ is needed to prove that real-time properties imply liveness properties. The desired liveness property for the timed queue is that the sequence of input messages up to any point eventually appears as the sequence of output messages. It is expressed by

Π_{Q}^{t} ∧ NZ ⇒ ∀ σ : □((hinp = σ) ⇒ ◇(hout = σ))

This formula is proved by first showing

Π_{Q}^{t} ∧ NZ ⇒ WF_{v}(EnQ) ∧ WF_{v}(DeQ)  (7)

and then using a standard liveness argument to prove

Π_{Q}^{t} ∧ WF_{v}(EnQ) ∧ WF_{v}(DeQ) ⇒ ∀ σ : □((hinp = σ) ⇒ ◇(hout = σ))

The proof that Π_{Q}^{t} ∧ NZ implies WF_{v}(EnQ) is by contradiction. Assume EnQ is forever enabled but never occurs. An invariance argument then shows that Π_{Q}^{t} implies that T_{EnQ} forever equals its current value, preventing now from advancing past that value; and this contradicts NZ . The proof that Π_{Q}^{t} ∧ NZ implies WF_{v}(DeQ) is similar.

3.3 The NonZeno Condition

The timed queue specification Π_{Q}^{t} asserts that a DeQ action must occur between δ_{snd} and Δ_{snd} seconds of when it becomes enabled. What if Δ_{snd} < δ_{snd}? If an input occurs, it eventually is put in the queue, enabling DeQ. At that point, the value of now can never become more than Δ_{snd} greater than its current value, so the program eventually reaches a “time-blocked state”. In a time-blocked state, only the QTick action can be enabled, and it cannot advance now past some fixed time. In other words, eventually a state is reached in which every variable other than now remains the same, and now either remains the same or keeps advancing closer and closer to some upper bound.

We can attempt to correct such pathological specifications by requiring that now increase without bound. This is easily done by conjoining the liveness property NZ to the safety property Π_{Q}^{t}, but that doesn’t accomplish anything. Since Π_{Q}^{t} ∧ NZ rules out behaviors in which now is bounded, it allows only behaviors in which there is no input, if Δ_{snd} < δ_{snd}. Such a specification is no better than the original specification Π_{Q}^{t}. The fact that the safety property allows the possibility of reaching a time-blocked state indicates an error in the specification. One does not add timing constraints on output actions with the intention of forbidding input.

We call a safety property Zeno if it allows the system to reach a state from which now must remain bounded. More precisely, a safety property Π is nonZeno iff every finite behavior satisfying Π can be completed to an infinite behavior satisfying Π in which now increases without bound. In other words, Π is nonZeno iff the pair (Π, NZ ) is machine closed.^{6}

Zenoness can be a source of incompleteness for proof methods. Only nonZeno behaviors are physically meaningful, so a real-time system with specification Π satisfies a property Ψ if Π ∧ NZ implies Ψ. As observed in Section 2.3, a proof

6An arbitrary property Π is nonZeno iff (C(Π), Π∧NZ ) is machine closed. We restrict our attention to real-time constraints for safety specifications.

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

method may be incapable of showing that Π ∧ NZ implies Ψ if (Π, NZ ) is not machine closed—that is, if Π is Zeno.

The following result can be used to ensure that a real-time specification written in terms of volatile δ-timers is nonZeno. The main hypotheses are: (1) the maximumdelay timers are on subactions of the untimed specification, and (3) a maximum delay for an action A_{j} is not smaller than a minimum delay for an action A_{i} if A_{i} and A_{j} can be simultaneously enabled.

Theorem 1. Let v be the tuple of variables free in Init or N. The property

∧ Init ∧ □[N]_{v} ∧ RT_{v}
∧ ∀i ∈ I : VTimer(t_{i}, A_{i}, δ_{i}, v) ∧ MinTime(t_{i}, A_{i}, v)
∧ ∀j ∈ J : VTimer(T_{j}, A_{j}, Δ_{j}, v) ∧ MaxTime(T_{j})

is nonZeno if now does not appear in v, I and J are finite sets, and for all i ∈ I and j ∈ J:

(1) ⟨A_{j}⟩_{v} is a subaction of Init ∧ □[N]_{v} whose free variables appear in v,

(2) δ_{i} and Δ_{j} are positive reals,

(3) δ_{i} ≤ Δ_{j}, or ⟨A_{i}⟩_{v} and ⟨A_{j}⟩_{v} are disjoint for Init ∧ □[N]_{v} and i ≠ j,

(4) the t_{i} and T_{j} are distinct variables different from now and from the variables in v.

We can apply the theorem to prove that the specification Π_{Q}^{t} is nonZeno if δ_{snd} ≤ Δ_{snd}. The hypotheses of the theorem are checked as follows.

(1) Actions ⟨DeQ⟩_{v} and ⟨EnQ⟩_{v} imply N_{Q}, so they are subactions of Π_{Q}.

(2) Trivial.

(3) The conjunction of any two of the actions ⟨Inp⟩_{v}, ⟨DeQ⟩_{v}, and ⟨EnQ⟩_{v} equals false, so the actions are pairwise disjoint for Π_{Q}.^{7} The only remaining cases to consider are those in which i = j. Only ⟨DeQ⟩_{v} has both a lower-bound and an upper-bound timer, and δ_{snd} ≤ Δ_{snd} holds by hypothesis.

(4) Trivial.

The theorem is valid for persistent as well as volatile timers. Any combination of VTimer and PTimer formulas may occur, except that a single A_{k} cannot have a persistent lower-bound timer t_{k} and a volatile upper-bound timer T_{k}. In fact, the theorem is valid for any kind of lower-bound timer t_{k}, not just a persistent or volatile one, provided t_{k} is never greater than the corresponding upper-bound timer T_{k}.

All of these results are corollaries of Theorem 2 below, which in turn is a consequence of Theorem 4 of Section 4. To allow arbitrary lower-bound timers, Theorem 2 uses different notation from Theorem 1. The Π of Theorem 2 corresponds to the conjunction of Init ∧ □[N]_{v} with all the VTimer formulas of Theorem 1.

Theorem 2. Let

—Π be a safety property of the form Init ∧ □[N]_{w},

7Actually, the type-correctness predicate T_{Q} is needed to prove that ⟨Inp⟩_{v} ∧ ⟨DeQ⟩_{v} equals false.

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

—t_{i} and T_{j} be timers for Π and let A_{k} be an action, for all i ∈ I, j ∈ J, and k ∈ I ∪ J, where I and J are sets, with J finite,

—Π^{t} =^{Δ} Π ∧ RT_{v} ∧ ∀ i ∈ I : MinTime(t_{i}, A_{i}, v) ∧ ∀ j ∈ J : MaxTime(T_{j})

If (1) Π^{t} ⇒ □(t_{i} ≤ T_{j}), or ⟨A_{i}⟩_{v} and ⟨A_{j}⟩_{v} are disjoint for Π and i ≠ j, for all i ∈ I and j ∈ J, (2) (a) now does not occur free in v, (b) (now′ = r) ∧ (v′ = v) is a subaction of Π, for all r ∈ R, (3) for all j ∈ J: (a) ⟨A_{j}⟩_{v} ∧ (now′ = now) is a subaction of Π, (b) Π ⇒ VTimer(T_{j}, A_{j}, Δ_{j}, v) or Π ⇒ PTimer(T_{j}, A_{j}, Δ_{j}, v), for some Δ_{j} ∈ ((0, ∞)), (c) Π^{t} ⇒ □(\begin{matrix}Enabled ⟨A_{j}⟩_{v} = \\ Enabled (⟨A_{j}⟩_{v} ∧ (now′ = now))) \end{matrix} (d) (v′ = v) ⇒ (Enabled ⟨A_{j}⟩_{v} = (Enabled ⟨A_{j}⟩_{v})′)

then (Π^{t}, NZ ) is machine closed

Most nonaxiomatic approaches, including both real-time process algebras and more traditional programming languages with timing constraints, essentially use δ-timers for actions. Theorem 2 implies that they automatically yield nonZeno specifications.

Theorem 2 can be further generalized in two ways. First, J can be infinite—if Π^{t} implies that only a finite number of actions A_{j} with j ∈ J are enabled before time r, for any r ∈ R. For example, by letting A_{j} be the action that sends message number j, we can apply the theorem to a program that sends messages number 1 through n at time n, for every integer n. This program is nonZeno even though the number of actions per second that it performs is unbounded. Second, we can extend the theorem to the more general class of timers obtained by letting the Δ_{j} be arbitrary real-valued state functions, rather than just constants—if all the Δ_{j} are bounded from below by a positive constant Δ.

Theorem 2 can be proved using Propositions 1 and 3 and ordinary TLA reasoning. By these propositions, it suffices to display a formula L that is the conjunction of fairness conditions on subactions of Π^{t} such that Π^{t} ∧ L implies NZ . A suitable L is WF_{(now,v)}(C), where C is an action that either (a) advances now by min_{j∈J} Δ_{j} if allowed by the upper-bound timers T_{j}, or else as far as they do allow, or (b) executes an ⟨A_{j}⟩_{v} action for which now = T_{j}. The proof in the appendix of Theorem 4, which implies Theorem 2, generalizes this approach.

Theorem 2 does not cover all situations of interest. For example, one can require of our timed queue that the first value appear on the output line within ϵ seconds of when it is placed on the input line. This effectively places an upper bound on the sum of the times needed for performing the EnQ and DeQ actions; it cannot be expressed with δ-timers on individual actions. For these general timing constraints, nonZenoness must be proved for the individual specification. The proof uses the method described above for proving Theorem 2: we add to the timed program Π^{t} a liveness property L that is the conjunction of any fairness properties we like, including fairness of the action that advances now, and prove that Π^{t} ∧ L implies NZ . NonZenoness then follows from Propositions 1 and 3.

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

There is another possible approach to proving nonZenoness. One can make granularity assumptions—lower bounds both on the amount by which now is incremented and on the minimum delay for each action. Under these assumptions, nonZenoness is equivalent to the absence of deadlock, which can be proved by existing methods. Granularity assumptions are probably adequate—after all, what harm can come from pretending that nothing happens in less than 10^{−100} nanoseconds? However, they can be unnatural and cumbersome. For example, distributed algorithms often assume that only message delays are significant, so the time required for local actions is ignored. The specification of such an algorithm should place no lower bound on the time required for a local action, but that would violate any granularity assumptions. We believe that any proof of deadlock freedom based on granularity can be translated into a proof of nonZenoness using the method outlined above.

So far, we have been discussing nonZenoness of the internal specification, where both the timers and the system’s internal variables are visible. Timers are defined by adding history-determined variables, so existentially quantifying over them preserves nonZenoness by Proposition 2. We expect most specifications to be fin [Abadi and Lamport 1991, page 263], so nonZenoness will also be preserved by existentially quantifying over the system’s internal variables. This is the case for the timed queue.

3.4 An Example: Fischer’s Protocol

As another example of real-time closed systems, we treat a simplified version of a real-time mutual exclusion protocol proposed by Fischer [1985] and described in [Lamport 1987, page 2]. The example was suggested by Schneider, Bloom, and Marzullo [1992]. The protocol consists of each process i executing the following code, where angle brackets denote instantaneous atomic actions:

a: await ⟨x = 0⟩;
b: ⟨x := i⟩;
c: await ⟨x = i⟩;
cs: critical section

There is a maximum delay Δ_{b} between the execution of the test in statement a and the assignment in statement b, and a minimum delay δ_{c} between the assignment in statement b and the test in statement c. The problem is to prove that, with suitable conditions on Δ_{b} and δ_{c}, this protocol guarantees mutual exclusion (at most one process can enter its critical section).

As written, Fischer’s protocol permits only one process to enter its critical section one time. The protocol can be converted to an actual mutual exclusion algorithm. The correctness proof of the protocol is easily extended to a proof of such an algorithm.

The TLA specification of the protocol is given in Figure 4. The formula Π_{F} describing the untimed version is standard TLA. We assume a finite set Proc of processes. Variable x represents the program variable x, and variable pc represents the control state. The value of pc will be an array indexed by Proc, where pc[i] equals one of the strings “a”, “b”, “c”, “cs” when control in process i is at the corresponding statement. The initial predicate Init_{F} asserts that pc[i] equals “a” for each process i, so the processes start with control at statement a. No assumption on the initial value of x is needed to prove mutual exclusion.

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

Init_{F} =^{Δ} ∀ i ∈ Proc : pc[i] = “a”

Go(i, u, v) =^{Δ} ∧ pc[i] = u

∧ pc′[i] = v
∧ ∀ j ∈ Proc : (j ≠ i) ⇒ (pc′[j] = pc[j])
A_{i} =^{Δ} Go(i, “a”, “b”) ∧ (x = x′ = 0)
B_{i} =^{Δ} Go(i, “b”, “c”) ∧ (x′ = i)
C_{i} =^{Δ} Go(i, “c”, “cs”) ∧ (x = x′ = i)
N_{F} =^{Δ} ∃ i ∈ Proc : (A_{i} ∨ B_{i} ∨ C_{i})
Π_{F} =^{Δ} Init_{F} ∧ □[N_{F}]_{(x,pc)}

Π_{F}^{t} =^{Δ} ∧ Π_{F} ∧ RT_{(x,pc)}

∧ ∀ i ∈ Proc : ∧ VTimer(T_{b}[i], B_{i}, Δ_{b}, (x, pc)) ∧ MaxTime(T_{b}[i])
∧ ∀ i ∈ Proc : ∧ VTimer(t_{c}[i], Go(i, “c”, “cs”), δ_{c}, (x, pc)) ∧ MinTime(t_{c}[i], C_{i}, (x, pc))
Φ_{F}^{t} =^{Δ} ∃ ∃ ∃ ∃ ∃ ∃ T_{b}, t_{c} : Π_{F}^{t}

Fig. 4. The TLA specification of Fischer’s real-time mutual exclusion protocol.

Next come the definitions of the three actions corresponding to program statements a, b, and c. They are defined using the formula Go, where Go(i, u, v) asserts that control in process i changes from u to v, while control remains unchanged in the other processes. Action A_{i} represents the execution of statement a by process i; actions B_{i} and C_{i} have the analogous interpretation. In this simple protocol, a process stops when it gets to its critical section, so there are no other actions. The program’s next-state action N_{F} is the disjunction of all these actions. Formula Π_{F} asserts that all processes start at statement a, and every step consists of executing the next statement of some process.

Action B_{i} is enabled by the execution of action A_{i}. Therefore, the maximum delay of Δ_{b} between the execution of statements a and b can be expressed by an upper-bound constraint on a volatile Δ_{b}-timer for action B_{i}. The variable T_{b} is an array of such timers, where T_{b}[i] is the timer for action B_{i}.

The constant δ_{c} is the minimum delay between when control reaches statement c and when that statement is executed. Therefore, we need an array t_{c} of lowerbound timers for the actions C_{i}. The delay is measured from the time control reaches statement c, so we want t_{c}[i] to be a δ_{c}-timer on an action that becomes enabled when process i reaches statement c and is not executed until C_{i} is. (Since we are placing only a lower-bound timer on it, the action need not be a subaction of Π_{F}.) A suitable choice for this action is Go(i, “c”, “cs”).

Adding these timers and timing constraints to the untimed formula Π_{F} yields formula Π_{F}^{t} of Figure 4, the specification of the real-time protocol with the timers visible. The final specification, Φ_{F}^{t}, is obtained by quantifying over the timer variables T_{b} and t_{c}. Since ⟨B_{j}⟩_{(x,pc)} ∧ (now′ = now) is a subaction of Π_{F} and ⟨Go(i, “c”, “cs”)⟩_{(x,pc)} is disjoint from ⟨B_{j}⟩_{(x,pc)}, for all i and j in Proc, Theorem 2 implies that Π_{F}^{t} is nonZeno if Δ_{b} is positive. Proposition 2 can then be applied to prove that Φ_{F}^{t} is nonZeno.

Mutual exclusion asserts that two processes cannot be in their critical sections

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

at the same time. It is expressed by the predicate

Mutex =^{Δ} ∀ i, j ∈ Proc : (pc[i] = pc[j] = “cs”) ⇒ (i = j)

The property to be proved is

Assump ∧ Φ_{F}^{t} ⇒ □Mutex  (8)

where Assump expresses the assumptions about the constants Proc, Δ_{b}, and δ_{c} needed for correctness. Since the timer variables do not occur in Mutex or Assump,

(8) is equivalent to

Assump ∧ Π_{F}^{t} ⇒ □Mutex

The standard method for proving this kind of invariance property leads to the invariant

∧ now ∈ R
∧ ∀ i ∈ Proc :

∧ T_{b}[i], t_{c}[i] ∈ R ∪ {∞} ∧ pc[i] ∈ {“a”, “b”, “c”, “cs”}

∧ (pc[i] = “cs”) ⇒ \begin{matrix}∧ x = i \\ ∧ ∀ j ∈ Proc : pc[j] ≠ “b” \end{matrix}

∧ (pc[i] = “c”) ⇒ \begin{matrix}∧ x ≠ 0 \\ ∧ ∀ j ∈ Proc : (pc[j] = “b”) ⇒ (t_{c}[i] > T_{b}[j]) \end{matrix}

∧ (pc[i] = “b”) ⇒ (T_{b}[i] < now + δ_{c})

∧ now ≤ T_{b}[i]

and the assumption

Assump =^{Δ} (0 ∉ Proc) ∧ (Δ_{b}, δ_{c} ∈ R) ∧ (Δ_{b} < δ_{c})

4. OPEN SYSTEMS

A closed system is solipsistic. An open system interacts with an environment, where system steps are distinguished from environment steps. Sections 4.1 and 4.2 reformulate a number of concepts introduced in [Abadi and Lamport 1993] that are needed for treating open systems in TLA. Some new results appear in Section 4.3. The following two sections explain how reasoning about open systems is reduced to reasoning about closed systems, and how open systems are composed.

4.1 Receptiveness and Realizability

To describe an open system in TLA, one defines an action μ such that μ steps are attributed to the system and ¬μ steps are attributed to the environment. A specification should constrain only system steps, not environment steps.

For safety properties, the concept of constraining is formalized as follows: if μ is an action and Π a safety property, then Π constrains at most μ iff, for any finite behavior s_{1}, …, s_{n} and state s_{n+1}, if s_{1}, …, s_{n} satisfies Π and (s_{n}, s_{n+1}) is a ¬μ step, then s_{1}, …, s_{n+1} satisfies Π. The generalization to arbitrary properties of constraining at most μ is μ-receptiveness. Intuitively, Π is μ-receptive iff every behavior in Π can be achieved by an implementation that performs only μ steps— the environment being able to perform any ¬μ step. The concept of receptiveness

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

is due to Dill [1988]. The generalization to μ-receptiveness is developed in [Abadi and Lamport 1993].^{8} A safety property is μ-receptive iff it constrains at most μ.

The generalization of machine closure to open systems is machine realizability. Intuitively, (Π, L) is μ-machine realizable iff an implementation that performs only μ steps can ensure that any finite behavior satisfying Π is completed to an infinite behavior satisfying Π ∧ L. Formally, (Π, L) is defined to be μ-machine realizable iff (Π, L) is machine closed and Π ∧ L is μ-receptive. For μ equal to true, machine realizability reduces to machine closure.

4.2 The −▷ Operator

A common way of specifying an open system is in terms of assumptions and guarantees [Jones 1983], requiring the system to guarantee a property M if its environment satisfies an assumption E. An obvious formalization of such a specification is the property E ⇒ M. However, this property contains behaviors in which the system violates M and then the environment later violates E. Because the system cannot predict what the environment will do, such behaviors cannot occur in any actual implementation. A behavior σ generated by any implementation satisfies the additional property that if any finite prefix of σ satisfies E, then it satisfies M. We can therefore formalize the assumption/guarantee specification by the property E −▷ M, defined by: σ ∈ E −▷ M iff σ ∈ (E ⇒ M) and, for every finite prefix ρ of σ, if ρ satisfies E then ρ satisfies M. If E and M are safety properties, then E −▷ M is as well.

For safety properties, the operator −▷ is the implication operator of an intuitionistic logic [Abadi and Plotkin 1992]. Most valid propositional formulas without negation remain valid when ⇒ is replaced by −▷, if all the formulas that appear on the left of a −▷ are safety properties. For example, the following formulas are valid if Φ and Π are safety properties.

Φ −▷ (Π −▷ Ψ) ≡ (Φ ∧ Π) −▷ Ψ
(Φ −▷ Ψ) ∧ (Π −▷ Ψ) ≡ (Φ ∨ Π) −▷ Ψ

(9)

For any TLA formulas Φ and Π, the property Φ −▷ Π is expressible as a TLA formula.

4.3 Proving Machine Realizability

Propositions 1–3, which concern machine closure, have generalizations for machine realizability. Proposition 1 is the special case of Proposition 4 in which Φ and μ are identically true. Proposition 3 is similarly a special case of Proposition 5 if (true, L_{2}) is machine closed—that is, if L_{2} is a liveness property. This is sufficient for our purposes, since NZ is a liveness property. The generalization of Proposition 2 is omitted; it would be analogous to Proposition 10 of [Abadi and Lamport 1993].

8To translate from the semantic model of [Abadi and Lamport 1993] into that of TLA, we let agents be pairs of states and identify an action μ with the set of all agents that are μ steps. A TLA behavior s_{1}, s_{2}, … corresponds to the sequence s_{1} ⟶^{α_{2}} s_{2} ⟶^{α_{3}} s_{3} ⟶^{α_{4}} …, where α_{i} equals (s_{i−1}, s_{i}). With this translation, the definitions in [Abadi and Lamport 1993] differ from the ones given here and in the appendix mainly by attributing the choice of initial state to the environment rather than to the system, requiring initial conditions to be assumptions about the environment rather than guarantees by the system.

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

Proposition 4 is stated in terms of μ-invariance, which generalizes the ordinary concept of invariance. A predicate P is a μ-invariant of a formula Π iff, in any behavior satisfying Π, no μ-step makes P false. This condition is expressed by the TLA formula Π ⇒ □[(μ ∧ P) ⇒ P′]_{P}.

Proposition 4. If Π and Φ are safety properties, Π constrains at most μ, and L is the conjunction of a finite or countably infinite number of formulas of the form WF_{w}(A) and/or SF_{w}(A), where, for each such formula,

(1) ⟨A⟩_{w} is a subaction of Π ∧ Φ,

(2) Π ∧ Φ ⇒ □[⟨A⟩_{w} ⇒ μ]_{w},

(3) if A appears in a formula SF_{w}(A), then Enabled ⟨A⟩_{w} is a ¬μ-invariant of Π ∧ Φ,

then (Φ −▷ Π, Φ ⇒ L) is μ-machine realizable.

Proposition 5. If Φ and Π are safety properties, (Φ −▷ Π, L_{1}) and (true, L_{2}) are μ-machine realizable, and Φ∧Π∧L_{1} implies L_{2}, then (Φ −▷ Π, L_{2}) is μ-machine realizable.

4.4 Reduction to Closed Systems

Consider a specification E −▷ M, where E and M are safety properties. We expect the system’s requirement to restrict only system steps, meaning that M constrains at most μ. This implies that E −▷ M also constrains at most μ. We also expect the environment assumption E not to constrain system steps; formally, E does not constrain μ iff it constrains at most ¬μ and it is satisfied by every (finite behavior consisting only of an) initial state.^{9}

Suppose E and M have the following form:

\begin{matrix}E & =^{Δ} & □[μ ∨ N_{E}]_{v} \\ M & =^{Δ} & Init ∧ □[¬μ ∨ N_{M}]_{v} \end{matrix}

Then E does not constrain μ and M constrains at most μ. If the system’s nextstate action N_{M} implies μ, and the environment’s next-state action N_{E} implies ¬μ, then a simple calculation shows that

E ∧ M ≡ Init ∧ □[N_{E} ∨ N_{M}]_{v}  (10)

Conjunction represents parallel composition, so E ∧M is the formula describing the closed system consisting of the open system together with its environment. Observe that E ∧ M has precisely the form we expect for a closed system comprising two components with next-state actions N_{E} and N_{M}.

We can make the inverse transformation from a closed system specification Π to the corresponding assumption/guarantee specification E −▷ M such that Π equals E ∧ M, where E does not constrain μ and M constrains at most μ. This is possible because any safety property Π can be written as such a conjunction.

Implementation means implication. A system with guarantee M implements a system with guarantee M̂, under environment assumption E, iff E −▷ M implies

9The asymmetry between constrains at most and does not constrain arises because we assign the system responsibility for the initial state.

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

E −▷ M̂. It follows from the definition of −▷ that, when E and M are safety properties, E −▷ M implies E −▷ M̂ iff E ∧ M implies E ∧ M̂. Thus, proving that one open system implements another is equivalent to proving the implementation relation for the corresponding closed systems. Implementation for open systems therefore reduces to implementation for closed systems.

4.5 Composition

The distinguishing feature of open systems is that they can be composed. The proof that the composition of two specifications implements a third specification is based on the following result, which is a reformulation of Theorem 2 of [Abadi and Lamport 1993] for safety properties.

Theorem 3. If E, E_{1}, E_{2},, M_{1}, and M_{2} are safety properties and μ_{1} and μ_{2} are actions such that

(1) E_{1} does not constrain μ_{1} and E_{2} does not constrain μ_{2},

(2) M_{1} constrains at most μ_{1} and M_{2} constrains at most μ_{2},

then the following proof rule is valid:

\frac{E ∧ M_{1} ∧ M_{2} ⇒ E_{1} ∧ E_{2}}{(E_{1} −▷ M_{1}) ∧ (E_{2} −▷ M_{2}) ⇒ (E −▷ M_{1} ∧ M_{2})}

This theorem is essentially the same as Theorem 1 of [Abadi and Plotkin 1992]; the proof is omitted.

5. REAL-TIME OPEN SYSTEMS

In Section 3, we saw how we can represent time by the variable now and introduce timing constraints with timers. To extend the method to open systems, we need only decide how to separate timing properties into environment assumptions and system guarantees. An examination of a paradoxical example in Section 5.1 leads to the general form described in Section 5.2, where the concept of nonZenoness is generalized.

5.1 A Paradox

Consider the two components Π_{1} and Π_{2} of Figure 5. Let the specification of Π_{1} be P_{y} −▷ P_{x}, which asserts that it writes a “good” sequence of outputs on x if its environment writes a good sequence of inputs on y. Let P_{x} −▷ P_{y} be the specification of Π_{2}, so Π_{2} writes a good sequence of outputs on y if its environment writes a good sequence of inputs on x. If P_{x} and P_{y} are safety properties, then it appears that we should be able to apply Theorem 3, our composition principle, to deduce that the composite system Π_{12} satisfies P_{x} ∧ P_{y}, producing good sequences of values on x and y. (We can define μ_{1} and μ_{2} so that writing on x is a μ_{1} action and writing on y is a μ_{2} action.)

Now, suppose P_{x} and P_{y} both assert that the value 0 is written by noon. These can be regarded as safety properties, since they assert that an undesirable event never occurs—namely, noon passing without a 0 having been written. Hence, the composition principle apparently asserts that Π_{12} sends 0’s along both x and y by noon. However, the specifications of Π_{1} and Π_{2} are satisfied by systems that wait for a 0 to be input, whereupon they immediately output a 0. The composition of those two systems does nothing.

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

[figure: Π_{1}; x; y; Π_{2}; x; y; x; y; Π_{12}]

Fig. 5. The composition of two systems.

This paradox depends on the ability of a system to respond instantaneously to an input. It is tempting to rule out such systems—perhaps even to outlaw specifications like these. We show that this Draconian measure is unnecessary. Indeed, if the specification of Π_{2} is strengthened to assert that a 0 must unconditionally be written on y by noon, then there is no paradox, and the composition does guarantee that a 0 is written on both x and y by noon. All paradoxes disappear when one carefully examines how the specifications must be written.

To resolve the paradox, we examine more closely the specifications S_{1} and S_{2} of Π_{1} and Π_{2}. For simplicity, let the only possible output actions be the setting of x and y to 0. The untimed version of S_{1} then asserts that, if the environment does nothing but set y to 0, then the system does nothing but set x to 0. This is expressed in TLA by letting

\begin{matrix}M_{x} & =^{Δ} & (x′ = 0) ∧ (y′ = y) & ν_{1} & =^{Δ} & x′ ≠ x \\ M_{y} & =^{Δ} & (y′ = 0) ∧ (x′ = x) \end{matrix}

and defining the untimed version of specification S_{1} to be

□[ν_{1} ∨ M_{y}]_{(x,y)} −▷ □[¬ν_{1} ∨ M_{x}]_{(x,y)}  (11)

To add timing constraints, we must first decide whether the system or the environment should change now. Since the advancing of now is a mythical action that does not have to be performed by any device, either decision is possible. Somewhat surprisingly, it turns out to be more convenient to let the system advance time. With the convention that initial conditions appear in the system guarantee, we define:

N_{x} =^{Δ} M_{x} ∧ (now′ = now)  MT_{x} =^{Δ} MaxTime(T_{x})
N_{y} =^{Δ} M_{y} ∧ (now′ = now)  MT_{y} =^{Δ} MaxTime(T_{y})
T_{x} =^{Δ} if x ≠ 0 then 12 else ∞ μ_{1} =^{Δ} ν_{1} ∨ (now′ ≠ now)
T_{y} =^{Δ} if y ≠ 0 then 12 else ∞
E_{1} =^{Δ} □[μ_{1} ∨ N_{y}]_{(x,y,now)}
M_{1} =^{Δ} (now = 0) ∧ □[¬μ_{1} ∨ N_{x}]_{(x,y,now)} ∧ RT_{(x,y)} ∧ MT_{x}

Adding timing constraints to (11) the same way we did for closed systems then

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

leads to the following timed version of specification S_{1}.

(E_{1} ∧ MT_{y}) −▷ M_{1}  (12)

However, this does not have the right form for an open system specification because MT_{y} constrains the advance of now, so the environment assumption constrains μ_{1}. The conjunct MT_{y} must be moved from the environment assumption to the system guarantee. Using (9), we rewrite (12) as:

S_{1} =^{Δ} E_{1} −▷ (MT_{y} −▷ M_{1})

This has the expected form for an open system specification, with an environment assumption E_{1} that does not constrain μ_{1} and a system guarantee MT_{y} −▷ M_{1} that constrains at most μ_{1}.

The specification S_{2} of the second component in Figure 5 is similar, where μ_{2}, E_{2}, M_{2}, and S_{2} are obtained from μ_{1}, E_{1}, M_{1}, and S_{1} by substituting 2 for 1, x for y, and y for x.

Both components Π_{1} and Π_{2} change now. This is not a problem because the components do not really control time. We have merely written the specifications S_{1} and S_{2} as if now were an output variable of both Π_{1} and Π_{2}. Formulas S_{1} and S_{2} express real-time constraints by making assertions about how now changes. There is no problem because these constraints do not conflict.

We now compose specifications S_{1} and S_{2}. The definitions of M_{1} and M_{2} and the observation that P −▷ Q implies P ⇒ Q yield

(MT_{x} ∨ MT_{y}) ∧ (MT_{y} −▷ M_{1}) ∧ (MT_{x} −▷ M_{2}) ⇒ M_{1} ∧ M_{2}  (13)

The definitions of M_{1} and M_{2} and simple temporal reasoning yield

E ∧ M_{1} ∧ M_{2} ⇒ E_{1} ∧ E_{2}  (14)

where

E =^{Δ} □[μ_{1} ∨ μ_{2}]_{(x,y,now)}

Combining (13) and (14) proves

E ∧ (MT_{x} ∨ MT_{y}) ∧ (MT_{y} −▷ M_{1}) ∧ (MT_{x} −▷ M_{2}) ⇒ E_{1} ∧ E_{2}

We can therefore apply Theorem 3, substituting E ∧ (MT_{x} ∨ MT_{y}) for E, MT_{y} −▷ M_{1} for M_{1}, and MT_{x} −▷ M_{2} for M_{2}, to deduce

S_{1} ∧ S_{2} ⇒ (E ∧ (MT_{x} ∨ MT_{y}) −▷ (MT_{y} −▷ M_{1}) ∧ (MT_{x} −▷ M_{2}) )

Using the implication-like properties of −▷, this simplifies to

S_{1} ∧ S_{2} ⇒ (E −▷ (MT_{y} −▷ M_{1}) ∧ (MT_{x} −▷ M_{2}))  (15)

All one can conclude about the composition from (15) is: either x and y are both 0 when now reaches 12, or neither of them is 0 when now reaches 12. There is no paradox.

As another example, we replace S_{2} by the specification E_{2} −▷ M_{2}. This specification, which we call S_{3}, asserts that the system sets y to 0 by noon, regardless of whether the environment sets x to 0. The definitions imply

MT_{y} ∧ E ∧ (MT_{y} −▷ M_{1}) ∧ M_{2} ⇒ E_{1} ∧ E_{2}

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

and Theorem 3 yields

S_{1} ∧ S_{3} ⇒ (E −▷ (MT_{x} −▷ M_{1}) ∧ M_{2})

Since M_{2} implies MT_{x}, this simplifies to

S_{1} ∧ S_{3} ⇒ (E −▷ M_{1} ∧ M_{2})

The composition of S_{1} and S_{3} does guarantee that both x and y equal 0 by noon.

5.2 Timing Constraints in General

Our no-longer-paradoxical example suggests that the form of a real-time open system specification should be

E −▷ (P −▷ M)  (16)

where M describes the system’s timing constraints and the advancing of now, and P describes the upper-bound timing constraints for the environment. Since the environment’s lower-bound timing constraints do not constrain the advance of now, they can remain in E. As we observed in Section 4.4, proving that one open specification implements another reduces to the proof for the corresponding closed systems. Since E −▷ (P −▷ M) is equivalent to (E ∧ P) −▷ M, the closed system corresponding to (16) is the expected one, E ∧ P ∧ M.

For the specification (16) to be reasonable, its closed system version, E ∧ P ∧ M, should be nonZeno. However, this is not sufficient. Consider a specification guaranteeing that the system produces a sequence of outputs until the environment sends a stop message, where the n^{th} output must occur by time (n − 1)/n. There is no timing assumption on the environment; it need never send a stop message. This is an unreasonable specification because now cannot reach 1 until the environment sends its stop message, so the advance of time is contingent on an optional action of the environment. However, the corresponding closed system specification is nonZeno, since time can always be made to advance without bound by having the environment send a stop message.

If advancing now is a μ action, then a system that controls μ actions can guarantee time to be unbounded while satisfying a safety specification S iff the pair (S, NZ ) is μ-machine realizable. We therefore take this condition to be the definition of nonZenoness for an open system specification S.

For specifications in terms of δ-timers, nonZenoness can be proved with generalizations to open systems of the theorems in Section 3.3. The following is the generalization of the strongest of them, Theorem 2. It is applied to a specification of the form (16) by substituting E ∧ P for E.

Theorem 4. With the notation and hypotheses of Theorem 2, if E and M are safety properties such that Π = E ∧ M, and

4. M constrains at most μ,

5. (a) ⟨A_{k}⟩_{v} ⇒ μ, for all k ∈ I ∪ J, (b) (now′ ≠ now) ⇒ μ

then (E −▷ M^{t}, NZ ) is μ-machine realizable, where

M^{t} =^{Δ} M ∧ RT_{v} ∧

∀ i ∈ I : MinTime(t_{i}, A_{i}, v) ∧ ∀ j ∈ J : MaxTime(T_{j})

Hypothesis 4 says that μ steps are attributed to the system represented by M. Part (a) of Hypothesis 5 says that the other hypotheses restrict the timing constraints on system actions ⟨A_{k}⟩_{v} only; environment actions may have any timing constraints. Part (b) says that advancing now is a system action.

The proof of Theorem 4, which appears in the appendix, is similar to the proof of Theorem 2 sketched in Section 3.3. It uses Propositions 4 and 5 instead of Propositions 1 and 3. Since machine realizability implies machine closure, Theorem 2 follows from Theorem 4 by letting E and μ equal true and M equal Π.

Theorem 4 applies to the internal specifications, where all variables are visible. For closed systems, existential quantification is handled with Proposition 2. For open systems, the generalization of this proposition—the analog of Proposition 10 of [Abadi and Lamport 1993]—is needed.

6. CONCLUSION

6.1 What We Did

We started with a simple idea—specifying and reasoning about real-time systems by representing time as an ordinary variable. This idea led to an exposition that most readers probably found quite difficult. What happened to the simplicity?

About half of the exposition is a review of concepts unrelated to real time. All the fundamental concepts described in Sections 2 and 4, including machine closure, machine realizability, and the −▷ operator, have appeared before [Abadi and Lamport 1993; Abadi and Lamport 1991]. These concepts are subtle, but they are important for understanding any concurrent system; they were not invented for real-time systems.

We chose to formulate these concepts in TLA. Like any language, TLA seems complicated on first encounter. We believe that a true measure of simplicity of a formal language is the simplicity of its formal description. The complete syntax and formal semantics of TLA are given in about one page in [Lamport 1991].

We never claimed that specifying and reasoning about concurrent systems is easy. Verifying concurrent systems is difficult and error prone. Our assertions that one formula follows from another, made so casually in the exposition, must be backed up by detailed calculations. We have omitted the proofs for our examples, which, done with the same detail as the proofs in the appendix, occupy some twenty pages.

We did claim that existing methods for specifying and reasoning about concurrent systems could be applied to real-time systems. Now, we can examine how hard they were to apply.

We found few obstacles in the realm of closed systems. The second author has more than fifteen years of experience in the formal verification of concurrent algorithms, and we knew that old-fashioned methods could be applied to real-time systems. However, TLA is relatively new, and we were pleased by how well it worked. The formal specification of Fischer’s protocol in Figure 4, obtained by conjoining timing constraints to the untimed protocol, is as simple and direct as we could have hoped for. Moreover, the formal correctness proofs of this protocol and of the queue example, using the method of reasoning described in [Lamport 1991], were straightforward. Perhaps the most profound discovery was the relation between nonZenoness and machine closure.

Open systems made up for any lack of difficulty with closed systems. State-based

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

approaches to open systems were a fairly recent development, and we had little experience with them. Studying real-time systems taught us a great deal, and led to a number of changes from the approach in [Abadi and Lamport 1993]. For example, we now write specifications with −▷ instead of ⇒, and we put initial conditions in the system guarantee rather than in the environment assumption. Many alternative ways of writing real-time specifications seemed plausible; choosing one that works was surprisingly hard. Even the simple idea of putting the environment’s timing assumptions to the left of a −▷ in the system’s guarantee came only after numerous failed efforts. Although the basic ideas we need to handle real-time open systems seem to be in place, we still have much to learn before reasoning about open systems becomes routine.

6.2 Beyond Real Time

Real-time systems introduce a fundamentally new problem: adding physical continuity to discrete systems. Our solution is based on the observation that, when reasoning about a discrete system, we can represent continuous processes by discrete actions. If we can pretend that the system progresses by discrete atomic actions, we can pretend that those actions occur at a single instant of time, and that the continuous change to time also occurs in discrete steps. If there is no system action between noon and \sqrt{2} seconds past noon, we can pretend that time advances by those \sqrt{2} seconds in a single action.

Physical continuity arises not just in real-time systems, but in “real-pressure” and “real-temperature” process-control systems. Such systems can be described in the same way as real-time systems: pressure and temperature as well as time are represented by ordinary variables. The continuous changes to pressure and temperature that occur between system actions are represented by discrete changes to the variables. The fundamental assumption is that the real, physical system is accurately represented by a model in which the system makes discrete, instantaneous changes to the physical parameters it affects.

The observation that continuous parameters other than time can be modeled by program variables has probably been known for years. However, the first published work we know of that uses this idea, by Marzullo, Schneider, and Budhiraja [1991], appeared only recently.

References

Abadi, M. and Lamport, L. 1991. The existence of refinement mappings.

Theoretical Computer Science 82, 2 (May), 253–284. Abadi, M. and Lamport, L. 1993. Composing specifications. ACM Transac-

tions on Programming Languages and Systems 15, 1 (Jan.), 73–132. Abadi, M. and Plotkin, G. 1992. A logical view of composition. Research

Report 86 (May), Digital Equipment Corporation, Systems Research Center. Alpern, B. and Schneider, F. B. 1985. Defining liveness. Information Pro-

cessing Letters 21, 4 (Oct.), 181–185. Apt, K. R., Francez, N., and Katz, S. 1988. Appraising fairness in languages

for distributed programming. Distributed Computing 2, 226–241. Bernstein, A. and Harter, Jr., P. K. 1981. Proving real time properties

of programs with temporal logic. In Proceedings of the Eighth Symposium on

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

Operating Systems Principles, New York, pp. 1–11. ACM. Operating Systems Review 15, 5.

Chandy, K. M. and Misra, J. 1988. Parallel Program Design. Reading, Mas-

sachusetts: Addison-Wesley. de Bakker, J. W., Huizing, C., de Roever, W. P., and Rozenberg, G.

(Eds.) 1992. Real-Time: Theory in Practice, Volume 600 of Lecture Notes in Computer Science. Berlin: Springer-Verlag. Proceedings of a REX Real-Time Workshop, held in The Netherlands in June, 1991.

Dill, D. L. 1988. Trace Theory for Automatic Hierarchical Verification of Speed-

Independent Circuits. Ph. D. thesis, Carnegie Mellon University. Fischer, M. 1985. Re: Where are you? E-mail message to Leslie Lam-

port. Arpanet message sent on June 25, 1985 18:56:29 EDT, number 8506252257.AA07636@YALE-BULLDOG.YALE.ARPA (47 lines).

Jones, C. B. 1983. Specification and design of (parallel) programs. In R. E. A. Mason (Ed.), Information Processing 83: Proceedings of the IFIP 9th World Congress, pp. 321–332. IFIP: North-Holland.

Lamport, L. 1982. An assertional correctness proof of a distributed algorithm.

Science of Computer Programming 2, 3 (Dec.), 175–206. Lamport, L. 1987. A fast mutual exclusion algorithm. ACM Transactions on

Computer Systems 5, 1 (Feb.), 1–11. Lamport, L. 1991. The temporal logic of actions. Research Report 79 (Dec.),

Digital Equipment Corporation, Systems Research Center. To appear in Transactions on Programming Languages and Systems.

Marzullo, K., Schneider, F. B., and Budhiraja, N. 1991. Derivation of sequential, real-time process-control programs. In A. M. van Tilborg and G. M. Koob (Eds.), Foundations of Real-Time Computing: Formal Specifications and Methods, Chapter 2, pp. 39–54. Boston, Dordrecht, and London: Kluwer Academic Publishers.

Misra, J. and Chandy, K. M. 1981. Proofs of networks of processes. IEEE

Transactions on Software Engineering SE-7, 4 (July), 417–426. Neumann, P. G. and Lamport, L. 1983. Highly dependable distributed sys-

tems. Technical report (June), SRI International. Contract Number DAEA18-81-G-0062, SRI Project 4180.

Pnueli, A. 1984. In transition from global to modular temporal reasoning about programs. In K. R. Apt (Ed.), Logics and Models of Concurrent Systems, NATO ASI Series, pp. 123–144. Springer-Verlag.

Schneider, F. B., Bloom, B., and Marzullo, K. 1992. Putting time into proof outlines. In J. W. de Bakker, C. Huizing, W.-P. de Roever, and G. Rozenberg (Eds.), Real-Time: Theory in Practice, Volume 600 of Lecture Notes in Computer Science, Berlin, Heidelberg, New York, pp. 618– 639. Springer-Verlag.

Appendix

An appendix to this paper is available in electronic form (Postscript^{TM}). At the moment, any of the following methods may be used to obtain it; the inside back cover of a current issue may contain more up-to-date instructions.

—By anonymous ftp from acm.org, file [pubs.journals.toplas.append]p1321.ps

—Send electronic mail to mailserve@acm.org containing the line

send [anonymous.pubs.journals.toplas.append]p1321.ps

—By Gopher from acm.org

—By anonymous ftp from ftp.cs.princeton.edu, file pub/toplas/append/p1321.ps

—Hardcopy from Article Express, for a fee: phone 800-238-3458, fax 201-216-8526, or write P.O. Box 1801, Hoboken NJ 07030; and request acm-toplas-appendix-

1321.

An Old-Fashioned Recipe for Real Time · A–1

The complete paper can be obtained by anonymous ftp from gatekeeper.dec.com. this document is the appendix to the following paper:

An Old-Fashioned Recipe for Real Time

MARTÍN ABADI and LESLIE LAMPORT Digital Equipment Corporation

Appendix

APPENDIX A. DEFINITIONS

A1 States and Behaviors

Σ: The set of all states (assignments of values to variables). Σ^{∗}: The set of finite behaviors (finite sequences of states). Σ^{∞}: The set of behaviors (infinite sequences of states). λ: The empty sequence. |σ| [for σ ∈ Σ^{∗} ∪ Σ^{∞}]: The length of σ. σ_{n} [for σ ∈ Σ^{∗} ∪ Σ^{∞} and 0 < n ≤ |σ|]: The n^{th} state in the sequence σ. σ|_{n} [for σ ∈ Σ^{∗} ∪ Σ^{∞} and 0 ≤ n ≤ |σ|]: The finite behavior σ_{1}, …, σ_{n}; equal to λ

when n = 0. σ ∘ s [for σ ∈ Σ^{∗} and s ∈ Σ]: The finite behavior σ_{1}, …, σ_{|σ|}, s. σ ≃ τ [for σ, τ ∈ Σ^{∗} or σ, τ ∈ Σ^{∞}]: σ and τ are equal except for stuttering steps

(repetitions of identical states).

σ ≃_{x} τ [for x a tuple of variables and either σ, τ ∈ Σ^{∗} or σ, τ ∈ Σ^{∞}]:

There exist behaviors σ̂ and τ̂ such that

∧ σ̂ ≃ σ and τ̂ ≃ τ

∧ |σ̂| = |τ̂|

∧ for every integer n ≤ |σ̂|, the states σ̂_{n} and τ̂_{n} are equal except for the values they assign to the variables of x.

A2 Predicates and Actions

predicate: A subset of Σ. state function: A mapping from Σ to the set of values. action: A subset of Σ × Σ. transition function: A mapping from Σ × Σ to the set of values. P′ [for P a predicate]: The action {(s, t) : t ∈ P }. f′ [for f a state function]: The transition function such that f′(s, t) = f(t). Enabled A [for A an action]: The predicate {s ∈ Σ : (∃t ∈ σ : (s, t) ∈ A)}. [A]_{f} [for A an action and f a state function]: A ∨ (f′ = f) ⟨A⟩_{f} [for A an action and f a state function]: ¬[¬A]_{f} (equals A ∧ (f′ ≠ f)).

Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, the ACM copyright notice and the title of the publication and its date appear, and notice is given that copying is by permission of the Association for Computing Machinery. To copy otherwise, or to republish, requires a fee and/or specific permission.

\begin{matrix}c \\ ◯ \end{matrix}1994 ACM

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

A–2 · Martín Abadi and Leslie Lamport

A3 Properties

property: A subset Π of Σ^{∞} such that for any σ, τ in Σ^{∞}, if σ ≃ τ then σ ∈ Π iff

τ ∈ Π.

□Π [for Π a property]:

The property {σ ∈ σ^{∞} : (∀n > 0 : σ_{n}, σ_{n+1}, … ∈ Π)}.

□[A]_{f} [for A an action and f a state function]:

The property {σ ∈ Σ^{∞} : (∀n > 0 : (σ_{n}, σ_{n+1}) ∈ [A]_{f})}. ◇Π [for Π a property or an action of the form ⟨A⟩_{f}]: ¬□¬Π Π ⇝ Φ [for Π and Φ properties]: □(Π ⇒ ◇Φ)

WF_{f}(A) [for f a state function and A an action]:

The property (□◇⟨A⟩_{f}) ∨ (□◇¬Enabled ⟨A⟩_{f}).

SF_{f}(A) [for f a state function and A an action]:

The property (□◇⟨A⟩_{f}) ∨ (◇□¬Enabled ⟨A⟩_{f}).

∃ ∃ ∃ ∃ ∃ ∃x : Π [for x a tuple of variables and Π a property]:

The property {σ ∈ Σ^{∞} : (∃ρ ∈ Π : ρ ≃_{x} σ)}.

A4 Closure and Safety

σ ⊧ Π [for σ ∈ Σ^{∗} and Π a property]:

There exists τ ∈ Π and n such that σ = τ|_{n}. C(Π) [for Π a property]: The property {σ ∈ Σ^{∞} : (∀n ≥ 0 : σ|_{n} ⊧ Π)}. safety property: A property Π such that Π = C(Π). (Π, L) machine closed [for Π and L properties]: Π = C(Π ∧ L) Φ −▷ Π [for Φ and Π properties]: The property consisting of all behaviors σ such

that ∧ σ ∈ Φ implies σ ∈ Π ∧ for all n ≥ 0: σ|_{n} ⊧ Φ implies σ|_{n} ⊧ Π.

A5 Realizability

Π constrains at most μ [for Π a safety property and μ an action]:

For any s ∈ Σ and ρ ∈ Σ^{∗} with |ρ| > 0, if ρ ⊧ Π and (ρ_{|ρ|}, s) ∉ μ, then ρ ∘ s ⊧ Π.

Π does not constrain μ [for Π a safety property and μ an action]:

Π constrains at most ¬μ, and every behavior of length 1 satisfies Π. μ-strategy [for μ an action]: A mapping f from Σ^{∗} to Σ ∪ {⊥} such that f(ρ) ≠ ⊥

implies (ρ_{|ρ|}, f(ρ)) ∈ μ, for any sequence ρ ∈ Σ^{∗} with ρ ≠ λ. O_{μ}(f) [for μ an action and f a μ-strategy]: The set of behaviors σ such that

∧ f(λ) = σ_{1} ∧ for all n > 0: (σ_{n}, σ_{n+1}) ∈ μ implies σ_{n+1} = f(σ|_{n}) ∧ for infinitely many n: f(σ|_{n}) = ⊥ or (σ_{n}, σ_{n+1}) ∈ μ.

O_{μ}(f, ρ) [for μ an action, f a μ-strategy, and ρ ∈ Σ^{∗}]: If ρ = λ then O_{μ}(f), else the set of behaviors σ such that ∧ ρ = σ|_{|ρ|} ∧ for all n ≥ |ρ|: (σ_{n}, σ_{n+1}) ∈ μ implies σ_{n+1} = f(σ|_{n}) ∧ for infinitely many n: f(σ|_{n}) = ⊥ or (σ_{n}, σ_{n+1}) ∈ μ.

Π is μ-receptive [for Π a property and μ an action]: For every behavior σ ∈ Π there

exists a μ-strategy f such that σ ∈ O_{μ}(f) and O_{μ}(f) ⊆ Π.

(Π, L) is μ-machine realizable [for Π and L properties and μ an action]:

(Π, L) is machine closed and Π ∧ L is μ-receptive.

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

APPENDIX B. PROOFS

B1 Proof Notation

We use hierarchically structured proofs. The theorem to be proved is statement ⟨0⟩1. 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. A proof may be preceded by a proof sketch, which informally describes the proof. Within a proof, ⟨k⟩l denotes the most recent statement with that number. A statement has the form

Assume: Assump Prove: Goal which is abbreviated to Goal if there is no assumption. The assertion Q.E.D. in statement number ⟨i + 1⟩k of the proof of statement ⟨i⟩j denotes the goal of statement ⟨i⟩j. The statement

Case: Assump is an abbreviation for

Assume: Assump Prove: Q.E.D. Within the proof of statement ⟨i⟩j, assumption ⟨i⟩ denotes that statement’s assumption, and ⟨i⟩.k denotes the assumption’s k^{th} item.

We recommend that proofs be read hierarchically, from the top level down. To read the proof of a long level-k step: (i) read the level-(k + 1) statements that comprise its proof, together with the proof of the final Q.E.D. step (which is usually a short paragraph), (ii) read the proof of each level-(k+1) step, in any desired order.

B2 Proof of Proposition 2

Assume: 1. (Π, L) is machine-closed.

2. x a tuple of variables, none of which occurs free in L.

3. ρ is a finite behavior satisfying ∃ ∃ ∃ ∃ ∃ ∃x : Π.

Prove: There exists an infinite behavior τ satisfying (∃ ∃ ∃ ∃ ∃ ∃x : Π) ∧ L such that ρ is

a prefix of τ.

⟨1⟩1. Choose a finite behavior σ satisfying Π such that σ ≃_{x} ρ.

⟨2⟩1. Choose a behavior ϕ such that ϕ ∈ ∃ ∃ ∃ ∃ ∃ ∃x : Π and ρ a prefix of ϕ.

Proof: Assumption ⟨0⟩.1. ⟨2⟩2. Choose a behavior ψ such that ψ ∈ Π and ψ ≃_{x} ϕ. Proof: ⟨2⟩1 and the definition of ∃ ∃ ∃ ∃ ∃ ∃x : Π.

⟨2⟩3. There exists an initial prefix σ of ψ such that σ ≃_{x} ρ.

Proof: ψ ≃_{x} ϕ (by ⟨2⟩2) and ρ a prefix of ϕ (by ⟨2⟩1). ⟨2⟩4. Q.E.D.

Proof: ⟨2⟩2 and ⟨2⟩3.

⟨1⟩2. Choose η satisfying Π ∧ L such that σ is a prefix of η.

Proof: The existence of τ follows from ⟨1⟩1 and assumption ⟨0⟩.1. ⟨1⟩3. Choose τ such that τ ≃_{x} η and ρ is a prefix of τ.

Proof: τ exists because σ is a prefix of η (by ⟨1⟩2) and σ ≃_{x} ρ (by ⟨1⟩1). ⟨1⟩4. τ satisfies ∃ ∃ ∃ ∃ ∃ ∃x : Π.

Proof: ⟨1⟩2, ⟨1⟩3, and the definition of ∃ ∃ ∃ ∃ ∃ ∃x : Π. ⟨1⟩5. τ satisfies L.

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

Proof: Steps ⟨1⟩4 and ⟨1⟩5 imply that τ satisfies (∃ ∃ ∃ ∃ ∃ ∃x : Π) ∧ L, and ρ is a prefix of τ by ⟨1⟩3.

B3 Proof of Proposition 3

Assume: 1. (Π, L_{1}) is machine closed.

2. Π ∧ L_{1} implies L_{2}.

Prove: (Π, L_{2}) is machine closed.

Proof: Π = C(Π ∧ L_{1}) [⟨0⟩.1] ⊆ C(Π ∧ L_{2}) [⟨0⟩.2 and monotonicity of closure] ⊆ C(Π)  [monotonicity of closure] = Π  [⟨0⟩.1, which implies Π closed]

This proves that Π = C(Π ∧ L_{2}).

B4 Two Lemmas About Machine-Realizability

Lemma 1. (Π, L) is μ-machine realizable iff for every finite behavior τ satisfying Π, there exists a μ-strategy f such that τ ⊧ O_{μ}(f) and O_{μ}(f) ⊆ Π ∧ L.

Proof: This is proved in Proposition 9 of [Abadi and Lamport 1993].

Lemma 2. (Π, L) is μ-machine realizable iff for every finite behavior τ satisfying Π, there exists a μ-strategy f such that O_{μ}(f, τ) ⊆ Π ∧ L.

⟨1⟩1. Assume: 1. For all finite τ such that τ ⊧ Π, there exists f_{τ} such that a. f_{τ} is a μ-strategy. b. O_{μ}(f_{τ} , τ) ⊆ Π ∧ L

2. ρ a finite behavior such that ρ ⊧ Π.

Prove: There exists a μ-strategy g such that ∧ ρ ⊧ O_{μ}(g)

∧ O_{μ}(g) ⊆ Π ∧ L

⟨2⟩1. Choose g such that, for all σ ∈ Σ^{∗}:

g(σ) =^{Δ} if (σ = ρ|_{n}) ∧ (n < |ρ|) then if (n = 0) ∨ (ρ_{n}, ρ_{n+1}) ∈ μ then ρ_{n+1} else ⊥ else f_{η}(σ), where η is the longest common prefix of ρ and σ

Proof: The requisite f_{η} exists by assumption ⟨0⟩.2, since ρ ⊧ Π implies η ⊧ Π, for any prefix η of ρ.

⟨2⟩2. g is a μ-strategy.

Proof: ⟨0⟩.1a and the the definition of g (⟨2⟩1). ⟨2⟩3. O_{μ}(g) ⊆ Π ∧ L

Proof: Assumption ⟨0⟩.1b, since κ ∈ O_{μ}(g) implies that κ ∈ O_{μ}(f_{η}, η), where η is the longest common prefix of κ and ρ.

⟨2⟩4. ρ ⊧ O_{μ}(g)

Proof: The definition of g implies that ρ is a prefix of an element of O_{μ}(g).

⟨2⟩5. Q.E.D.

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

⟨1⟩2. Assume: (Π, L) is μ-machine realizable and τ ⊧ Π.

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

Prove: There exists a μ-strategy f such that O_{μ}(f, τ) ⊆ Π ∧ L.

⟨2⟩1. Choose a μ-strategy f such that τ ∈ O_{μ}(f) and O_{μ}(f) ⊆ Π ∧ L. Proof: Assumption ⟨2⟩ and Lemma 1.

⟨2⟩2. O_{μ}(f, τ) ⊆ Π ∧ L

Proof: ⟨2⟩1.2 and the definition of O_{μ}(f, τ).

⟨2⟩3. Q.E.D.

Proof: ⟨2⟩1 and ⟨2⟩2.

⟨1⟩3. Q.E.D.

Proof: By ⟨1⟩1, ⟨1⟩2 and Lemma 1.

B5 Proof of Proposition 4

Let: Ψ =^{Δ} Φ ∧ Π

L =^{Δ} \begin{matrix}∧ ∀i ∈ I : WF_{w_{i}}(A_{i}) \\ ∧ ∀j ∈ J : SF_{w_{j}}(A_{j}) \end{matrix}

Assume: 1. Φ and Π are safety properties.

2. Π constrains at most μ.

3. I ∪ J a finite or countably infinite set, which we take to be a set of natural numbers.

4. For all k in I ∪ J:

a. ⟨A_{k}⟩_{w_{k}} is a subaction of Ψ. b. Ψ ⇒ □[⟨A_{k}⟩_{w_{k}} ⇒ μ]_{w_{k}}

5. Forall j in J: Enabled ⟨A_{j}⟩_{w_{j}} is a ¬μ invariant of Ψ.

Prove: (Φ −▷ Π, Φ ⇒ L) is μ-machine realizable. By Lemma 2, it suffices to Assume: 6. τ ⊧ Φ −▷ Π Prove: There exists a μ-strategy f such that

O_{μ}(f, τ) ⊆ (Φ −▷ Π) ∧ (Φ ⇒ L).

Proof sketch: Defining the strategy f is tantamount to constructing a scheduler that executes the actions ⟨A_{k}⟩_{w_{k}} to satisfy the fairness requirements. Action ⟨A_{k}⟩_{w_{k}} is never considered until k steps have occurred, so only finitely many actions are considered at any point. The next action scheduled is the enabled action that has been under consideration for the longest time without having been executed. In the event of ties, the lowest-numbered action is chosen. The strategy f will never violate Ψ, and it stops making moves if Ψ is ever made false by the environment. In the following definitions, nextact(ρ) is the k such that the scheduler chooses to execute ⟨A_{k}⟩_{w_{k}} after the finite behavior ρ.

Let: B_{k} =^{Δ} ⟨A_{k}⟩_{w_{k}}

n =^{Δ} |τ|

lasttime(ρ, k) =^{Δ} max ({l : 1 < l ≤ |ρ| : (ρ_{l−1}, ρ_{l}) ∈ B_{k}} ∪ {k})

able(ρ)  =^{Δ} if ρ = λ then the set of naturals else {k : ρ_{|ρ|} ∈ Enabled B_{k}}

oldestlast(ρ) =^{Δ} min{lasttime(ρ, k) : k ∈ able(ρ)}

nextact(ρ) =^{Δ} min{k ∈ able(ρ) : lasttime(ρ, k) = oldestlast(ρ)}

⟨1⟩1. Choose f such that for all ρ in Σ^{∗}:

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

if (able(ρ) = ∅) ∨ (ρ ∉ Ψ)

then f(ρ) = ⊥

else

∧ (ρ ≠ λ) ⇒ (ρ_{|ρ|}, f(ρ)) ∈ B_{nextact(ρ)}
∧ ρ ∘ f(ρ) ∈ Ψ

Proof sketch: We must show that, for any ρ, the requisite f(ρ) exists. ⟨2⟩1. Assume: (able(ρ) ≠ ∅) ∧ ρ ⊧ Ψ

Prove: ∃ s ∈ Σ : ∧ (ρ ≠ λ) ⇒ (ρ_{|ρ|}, s) ∈ B_{nextact(ρ)} ∧ ρ ∘ s ∈ Ψ

⟨3⟩1. Case: ρ = λ Proof: Assumption ⟨2⟩ and the definition of ρ ⊧ Ψ. ⟨4⟩1. Case: ρ ≠ λ

⟨5⟩1. ρ_{|ρ|} ∈ Enabled B_{nextact(ρ)} ⟨6⟩1. nextact(ρ) ∈ able(ρ)

Proof: Assumption ⟨2⟩ and the definitions of nextact and oldestlast. ⟨6⟩2. Q.E.D.

Proof: Case assumption ⟨4⟩ and the definition of able(ρ). ⟨5⟩2. Q.E.D.

Proof: ⟨5⟩1 and Assumption ⟨0⟩.4a. ⟨4⟩2. Q.E.D.

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

Proof: The existence of the required f follows easily from ⟨2⟩1. ⟨1⟩2. f is a μ-strategy.

Assume: (ρ ≠ λ) ∧ (f(ρ) ≠ ⊥) Prove: (ρ_{|ρ|}, f(ρ)) ∈ μ Proof: ⟨1⟩1 and assumption ⟨1⟩ imply

∧ (ρ_{|ρ|}, f(ρ)) ∈ B_{nextact(ρ)}

∧ ρ ∘ f(ρ) ⊧ Ψ

and the result follows from ⟨0⟩.4b. ⟨1⟩3. O_{μ}(f, τ) ⊆ (Φ −▷ Π)

Proof sketch: This is a straightforward induction proof; ⟨2⟩1 is the base case and ⟨2⟩2 is the induction step. ⟨2⟩1. Assume: σ ∈ O_{μ}(f, τ)

Prove: σ|_{0} ⊧ Φ −▷ Π Proof: σ|_{0} = τ|_{0}, and τ ⊧ (Φ −▷ Π) by assumption ⟨2⟩ and the definition of O_{μ}(f, τ).

⟨2⟩2. Assume: 1. σ ∈ O_{μ}(f, τ)

2. σ|_{i} ⊧ Φ −▷ Π

3. i ≥ 0

Prove: σ|_{i+1} ⊧ Φ −▷ Π ⟨3⟩1. Case: i ≥ |τ|

⟨4⟩1. Case: (σ_{i}, σ_{i+1}) ∉ μ Proof: Follows easily from assumption ⟨2⟩.2 and assumption ⟨0⟩.2, since Π constrains at most μ implies Φ −▷ Π constrains at most μ.

⟨4⟩2. Case: (σ_{i}, σ_{i+1}) ∈ μ ⟨5⟩1. σ_{i+1} = f(σ|_{i})

Proof: Assumption ⟨2⟩.1. ⟨5⟩2. Q.E.D.

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

Proof: ⟨5⟩1, assumption ⟨2⟩.2, and the else clause in ⟨1⟩1 (the definition of f).

⟨4⟩3. Q.E.D.

Proof: ⟨4⟩1 and ⟨4⟩2. ⟨3⟩2. Case: i < |τ|

Proof: By assumption ⟨0⟩.6 and assumption ⟨2⟩.1, since i < |τ| implies σ|_{i+1} = τ|_{i+1}.

⟨3⟩3. Q.E.D.

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

Proof: ⟨2⟩1, ⟨2⟩2, mathematical induction, and assumption ⟨0⟩.1. ⟨1⟩4. O_{μ}(f, τ) ⊆ (Φ ⇒ L)

Proof sketch: The proof is by contradiction. We define IE and IO to be the sets of indices of actions that should be executed infinitely often and that actually are executed infinitely often, respectively. We show that the existence of a q in IE but not in IO leads to a contradiction. Assume: 1. σ ∈ O_{μ}(f, τ)

2. σ ∈ Φ

3. ∃ k ∈ I ∪ J : \begin{matrix}a.∨ k ∈ I ∧ σ ∉ WF_{w_{k}}(A_{k}) \\ b.∨ k ∈ J ∧ σ ∉ SF_{w_{k}}(A_{k}) \end{matrix}

Prove: false Let:

IE =^{Δ} {i ∈ I : ◇□Enabled B_{i}} ∪ {j ∈ J : □◇Enabled B_{j}}
IO =^{Δ} {k ∈ I ∪ J : (σ_{n}, σ_{n+1}) ∈ B_{k} for infinitely many n}

⟨2⟩1. σ ∈ Φ ∧ Π

Proof: ⟨1⟩3 and assumption ⟨1⟩.1, which imply σ ∈ Φ −▷ Π, and ⟨1⟩.2. ⟨2⟩2. Choose q such that

1. q ∈ IE

2. q ∉ IO Proof: Assumption ⟨1⟩.3.

⟨2⟩3. Choose m_{1} such that 1. m_{1} > q

2. ∀n ≥ m_{1} : (σ_{n−1}, σ_{n}) ∉ B_{q}

3. m_{1} > |τ| Proof: ⟨2⟩2.2

⟨2⟩4. Choose m_{2} such that 1. m_{2} > m_{1}

2. ∀k ∈ I ∪ J : (k ∉ IO) ∧ (k < m_{1}) ⇒ ∀n > m_{2} : (σ_{n}, σ_{n+1}) ∉ B_{k} Proof: Definition of IO.

⟨2⟩5. Choose m_{3} such that 1. m_{3} > m_{2}

2. ∀k ∈ I ∪ J : (k ∈ IO) ∧ (k < m_{1}) ⇒

∃ n > m_{2} : (n < m_{3}) ∧ (σ_{n}, σ_{n+1}) ∈ B_{k}

Proof: Definition of IO. ⟨2⟩6. Choose m_{4} such that

1. m_{4} > m_{3}

2. σ_{m_{4}} ∈ Enabled B_{q}

3. (q ∈ I) ⇒ ∀n > m_{4} : σ_{n} ∈ Enabled B_{q} Proof: ⟨2⟩2.1 and the definition of IE.

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

⟨2⟩7. ∀n > m_{4} : \begin{matrix}1.∧ σ_{n} ∈ Enabled B_{q} \\ 2.∧ (σ_{n−1}, σ_{n}) ∉ μ \end{matrix}

Proof sketch: By time m_{4}, B_{q} is the next action scheduled for execution. Since B_{q} is never again executed (by ⟨2⟩3), there can be no further μ steps. Since only a μ step can disable B_{q} (by assumption ⟨0⟩.5), B_{q} must be enabled forever. The formal proof is by induction on n; ⟨3⟩1 is the base case and ⟨3⟩2 is the induction step. ⟨3⟩1. σ_{m_{4}} ∈ Enabled B_{q}

Proof: ⟨2⟩6. ⟨3⟩2. Assume: 1. σ_{n} ∈ Enabled B_{q}

2. (σ_{n−1}, σ_{n}) ∉ μ

3. n ≥ m_{4}
Prove: \begin{matrix}∧ σ_{n+1} ∈ Enabled B_{q} \\ ∧ (σ_{n}, σ_{n+1}) ∉ μ \end{matrix}

⟨4⟩1. (σ_{n}, σ_{n+1}) ∉ μ Assume: (σ_{n}, σ_{n+1}) ∈ μ Prove: false

⟨5⟩1. ∨ nextact(σ|_{n}) = q

∨ ∃ k ∈ I ∪ J : ∧ nextact(σ|_{n}) = k ∧ k < m_{1} ∧ k ∉ IO ∧ k ∈ able(σ|_{n})

⟨6⟩1. q ∈ able(σ|_{n})

Assumption ⟨3⟩.1. ⟨6⟩2. Assume: k ≥ m_{1}

Prove: lasttime(σ|_{n}, k) > lasttime(σ|_{n}, q) Proof: lasttime(σ|_{n}, k) ≥ m_{1} by definition of lasttime, and m_{1} > lasttime(σ|_{n}, q) by assumption ⟨3⟩.1.

⟨6⟩3. Assume: (k > m_{1}) ∧ (k ∈ IO)

Prove: lasttime(σ|_{n}, k) > lasttime(σ|_{n}, q) Proof: lasttime(σ|_{n}, k) ≥ m_{2} > m_{1} by ⟨2⟩5, and m_{1} > lasttime(σ|_{n}, q) by assumption ⟨3⟩.1.

⟨6⟩4.

∨ oldestlast(σ|_{n}) = q

∨ ∃ k ∈ I ∪ J : ∧ oldestlast(σ|_{n}) = k ∧ k < m_{1} ∧ k ∉ IO ∧ k ∈ able(σ|_{n})

Proof: ⟨6⟩1, ⟨6⟩2, and ⟨6⟩3. ⟨6⟩5. Q.E.D.

Proof: ⟨6⟩4 and definition of nextact.

⟨5⟩2. \begin{matrix}∨ (σ_{n}, σ_{n+1}) ∈ B_{q} \\ ∨ ∃ k ∈ I ∪ J : \begin{matrix}∧ (σ_{n}, σ_{n+1}) ∈ B_{k} \\ ∧ k < m_{1} ∧ k ∉ IO \end{matrix} \end{matrix}

Proof: ⟨5⟩1, the definition of f (⟨1⟩1), assumption ⟨4⟩, and assumption ⟨1⟩.1, since n > |τ| by assumption ⟨3⟩.3 and ⟨2⟩3–⟨2⟩6.

⟨5⟩3. Q.E.D.

⟨6⟩1. Case: (σ_{n}, σ_{n+1}) ∈ B_{q} Proof: Contradicts ⟨2⟩3, since n > m_{1} by assumption ⟨3⟩.3 and ⟨2⟩4–⟨2⟩6.

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

⟨6⟩2. Case: ∃ k ∈ I ∪ J : \begin{matrix}∧ (σ_{n}, σ_{n+1}) ∈ B_{k} \\ ∧ k < m_{1} ∧ k ∉ IO \end{matrix}

Proof: Contradicts ⟨2⟩4, since n > m_{2} by assumption ⟨3⟩.3, ⟨2⟩5, and ⟨2⟩6.

⟨6⟩3. Q.E.D.

Proof: ⟨6⟩1 and ⟨6⟩2. ⟨4⟩2. σ_{n+1} ∈ Enabled B_{q}

Proof: Assumption ⟨3⟩.1, ⟨4⟩1, ⟨2⟩1, and assumption ⟨0⟩.5. ⟨4⟩3. Q.E.D.

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

Proof: ⟨3⟩1, ⟨3⟩2, and mathematical induction. ⟨2⟩8. Q.E.D.

⟨3⟩1. ∀n > m_{4} : f(σ|_{n}) ≠ ⊥

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

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

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

B6 Proof of Proposition 5

Assume: 1. Φ and Π are safety properties.

2. (Φ −▷ Π, L_{1}) is μ-machine realizable.

3. (true, L_{2}) is μ-machine realizable.

4. Φ ∧ Π ∧ L_{1} implies L_{2}.

Prove: (Φ −▷ Π, L_{2}) is μ-machine realizable. ⟨1⟩1. Assume: ρ is a finite behavior such that ρ ⊧ (Φ −▷ Π).

Prove: There exists a μ-strategy f such that

O_{μ}(f, ρ) ⊆ (Φ −▷ Π) ∧ L_{2}.

⟨2⟩1. Choose μ-strategy h such that O_{μ}(h, ρ) ⊆ (Φ −▷ Π) ∧ L_{1}.

Proof: Assumption ⟨0⟩.2, assumption ⟨1⟩, and Lemma 2. ⟨2⟩2. For all τ, choose a μ-strategy g_{τ} such that O_{μ}(g_{τ} , τ) ⊆ L_{2}.

Proof: Assumption ⟨0⟩.3 and Lemma 2. ⟨2⟩3. Let f(τ) = h(τ) for τ ⊧ Φ, and otherwise let f(τ) = g_{η}(τ) where η is

the shortest prefix of τ such that η |̸= Φ. Then f is a μ-strategy. Proof: By steps ⟨2⟩1 and ⟨2⟩2 (which say that h and g_{η} are μ-strategies).

⟨2⟩4. O_{μ}(f, ρ) ⊆ (Φ −▷ Π) ∧ L_{2} Assume: τ ∈ O_{μ}(f, ρ) Prove: τ ∈ (Φ −▷ Π) ∧ L_{2} ⟨3⟩1. Case: τ ∈ Φ

⟨4⟩1. τ ∈ O_{μ}(h, ρ)

Proof: By assumption ⟨2⟩, since the case assumption ⟨3⟩ and the definition of f (step ⟨2⟩3) imply f(τ|_{n}) = h(τ|_{n}) for all n.

⟨4⟩2. τ ∈ (Φ −▷ Π) ∧ L_{1}

Proof: By step ⟨4⟩1 and the choice of h (step ⟨2⟩1). ⟨4⟩3. τ ∈ Φ ∧ Π ∧ L_{1}

Proof: By step ⟨4⟩2 and case assumption ⟨3⟩.

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

⟨4⟩4. Q.E.D.

Proof: By step ⟨4⟩3 and assumption ⟨0⟩.4.

⟨3⟩2. Case: τ ∉ Φ

⟨4⟩1. Let n be the least integer such that τ|_{n} ∉ Φ. Proof: Such an n exists by case assumption ⟨3⟩ and assumption ⟨0⟩.1. ⟨4⟩2. τ ∈ O_{μ}(g_{τ|_{n}}, τ|_{n})

Proof: By step ⟨4⟩1, assumption ⟨2⟩, and the definition of f (step ⟨2⟩3).

⟨4⟩3. τ ∈ L_{2}

Proof: By steps ⟨4⟩2 and the choice of g_{τ|_{n}} (step ⟨2⟩2). ⟨4⟩4. Q.E.D.

Proof: By steps ⟨4⟩3 and case assumption ⟨3⟩.

⟨3⟩3. Q.E.D.

Proof: By steps ⟨3⟩1 and ⟨3⟩2.

⟨2⟩5. Q.E.D.

Proof: By steps ⟨2⟩3 and ⟨2⟩4.

⟨1⟩2. Q.E.D.

Proof: The result follows immediately from step ⟨1⟩1 and Lemma 2.

B7 Proof of Theorem 4

The proof of Theorem 4 is rather long and is presented in two steps. Section B7.1 contains a high-level view of the proof; Section B7.2 contains the complete proof, omitting definitions and complete subproofs that appear in the high-level view. If a formula F is a conjunction, we may number the conjuncts and let F.i denote the i^{th} one.

The proof uses the following two lemmas.

Lemma Rule WF1. For any predicates P, Q, and I; actions N and A; and state function f; if

(1) P ∧ I ∧ I′ ∧ [N]_{f} ⇒ (P′ ∨ Q′)

(2) P ∧ I ∧ I′ ∧ ⟨N ∧ A⟩_{f} ⇒ Q′

(3) P ∧ I ⇒ Enabled ⟨A⟩_{f}. then WF_{f}(A) ∧ □I ∧ □[N]_{f} ⇒ (P ⇝ Q)

Proof: This is a simple generalization of rule WF1 of [Lamport 1991]; the proof of soundness is omitted.

Lemma 4. For any actions A and B, state function f, variable x, predicate P, and property Π:

(1) (a) (Enabled (x′ = f)) = true.

(b) If A and B have no primed variables in common, then (Enabled A ∧ B) = (Enabled A) ∧ (Enabled B).

(2) (Enabled A) ∧ (¬Enabled B) ⇒ (Enabled A ∧ ¬B)

(3) (Enabled P ∧ A) = (P ∧ Enabled A)

(4) (Enabled ∃ x : A) = (∃ x : Enabled A)

(5) If A ⇒ B then (Enabled A) ⇒ (Enabled B).

Proof: These properties all follow easily from the definitions.

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

B7.1 High-Level Proof of the Theorem

Let: Π =^{Δ} E ∧ M

M^{t} =^{Δ} M ∧ RT_{v} ∧
∀ i ∈ I : MinTime(t_{i}, A_{i}, v) ∧ ∀ j ∈ J : MaxTime(T_{j})
Π^{t} =^{Δ} E ∧ M^{t}

Assume: 0. a. Π = Init ∧ □[N]_{w} for some predicate Init, action N, and state

function w. b. t_{i} is a timer for Π, for all i in I. c. T_{j} is a timer for Π, for all j in J. d. J is a finite set.

1. Π^{t} ⇒ □(t_{i} ≤ T_{j}), or ⟨A_{i}⟩_{v} and ⟨A_{j}⟩_{v} are disjoint for Π and i ≠ j, for all i ∈ I and j ∈ J.

2. a. now does not occur free in v.

b. (now′ = r) ∧ (v′ = v) is a subaction of Π, for all r ∈ R.

3. For all j ∈ J:

a. ⟨A_{j}⟩_{v} ∧ (now′ = now) is a subaction of Π, b. Π ⇒ VTimer(T_{j}, A_{j}, Δ_{j}, v) or Π ⇒ PTimer(T_{j}, A_{j}, Δ_{j}, v), for

some Δ_{j} ∈ ((0, ∞)), c. Π^{t} ⇒ □(Enabled ⟨A_{j}⟩_{v} = Enabled (⟨A_{j}⟩_{v} ∧ (now′ = now))) d. (v′ = v) ⇒ (Enabled ⟨A_{j}⟩_{v} = (Enabled ⟨A_{j}⟩_{v})′)

4. E and M are safety properties, and M constrains at most μ.

5. a. ⟨A_{k}⟩_{v} ⇒ μ, for all k ∈ I ∪ J.

b. (now′ ≠ now) ⇒ μ

Prove: (E −▷ M^{t}, NZ ) is μ-machine realizable. Proof sketch: We show that a fairness condition WF_{(now,v)}(C) implies that now increases without bound, for a subaction ⟨C⟩_{(now,v)} of Π^{t}, and then apply Propositions 4 and 5. To prove that now increases without bound, we prove that now = r leads to now ≥ (r + Δ) for any number r, where Δ is the minimum of the Δ_{j}. The action C advances now or, if that is impossible because now = T_{j} for some upper-bound timer T_{j}, it performs the action A_{j} (thereby advancing T_{j}). We begin by naming the next-state relations of the RT_{v}, MaxTime, MinTime, VTimer, and PTimer formulas and defining some actions and predicates, including C. A B_{j} step is defined to be an A_{j} step that leaves now unchanged. An A_{j}^{t} step is an A_{j} step that satisfies the lower-bound timing constraint, if there is one. A B_{j}^{t} step is a B_{j} step taken when T_{j} equals now that satisfies the lower-bound timing constraint, if there is one. The state function T is the smallest T_{j} that restricts the advance of now.

Let: RTact_{v}  =^{Δ} [(now′ ∈ ((now, ∞))) ∧ (v′ = v)]_{now}
MaxTact(t)  =^{Δ} [now′ ≤ t′]_{now}

MinTact(t, A, v) =^{Δ} [A ⇒ (t ≤ now)]_{v}

VTact(t, A, δ, v) =^{Δ} [\begin{matrix}∧ t′ = if (Enabled ⟨A⟩_{v})′ then if ⟨A⟩_{v} ∨ ¬Enabled ⟨A⟩_{v} then now + δ else t else ∞ \\ ∧ v′ ≠ v]_{(t,v)} \end{matrix} PTact(t, A, δ, v) =^{Δ} [\begin{matrix}∧ t′ = if Enabled ⟨A⟩_{v} then if ⟨A⟩_{v} then now + δ else t else t + (now′ − now) \\ ∧ (now, v)′ ≠ (now, v)]_{(t,v,now)} \end{matrix}

P_{j} =^{Δ} (j ∈ I) ⇒ (t_{j} ≤ now)

A_{j}^{t} =^{Δ} A_{j} ∧ P_{j}

B_{j} =^{Δ} A_{j} ∧ (now′ = now)

B_{j}^{t} =^{Δ} A_{j}^{t} ∧ (now′ = now) ∧ (T_{j} = now)

T =^{Δ} min{T_{j} : j ∈ J ∧ Enabled ⟨A_{j}⟩_{v}}

Δ =^{Δ} min{Δ_{j} : j ∈ J}

NowT =^{Δ} (now′ = min(now + Δ, T)) ∧ (v′ = v)

C  =^{Δ} ∨ (T ≠ now) ∧ NowT ∨ (T = now) ∧ ∃ j ∈ J : B_{j}^{t}

⟨1⟩1. Choose J_{P} and J_{V} such that:

1. J = J_{P} ∪ J_{V}

2. J_{P} ∩ J_{V} = ∅

3. ∀j ∈ J_{V} : Π ⇒ VTimer(T_{j}, A_{j}, Δ_{j}, v)

4. ∀j ∈ J_{P} : Π ⇒ P T imer(T_{j}, A_{j}, Δ_{j}, v) Proof: J_{P} and J_{V} exist by assumption ⟨0⟩.3b.

⟨1⟩2. Π^{t} ⇒ □Inv, where Inv =^{Δ} 1.∧ ∀j ∈ J : T_{j} ∈ [[now, ∞]] 2.∧ now ∈ R 3.∧ ∀j ∈ J : (Enabled ⟨A_{j}⟩_{v} = Enabled (⟨A_{j}⟩_{v} ∧ (now′ = now)) 4.∧ ∀k ∈ I ∩ J : t_{k} ≤ T_{k} 5.∧ ∀j ∈ J_{V} : ¬Enabled ⟨A_{j}⟩_{v} ⇒ (T_{j} = ∞)

Proof sketch: It follows immediately from the hypotheses that Π^{t} implies □Inv.3 and □Inv.4. The proofs for the other conjuncts of Inv are straightforward but somewhat tedious invariance proofs, which are omitted. ⟨2⟩1. RT_{v} ⇒ □Inv.2

⟨2⟩2. For all j ∈ J : Π ∧ □Inv.2 ∧ MaxTime(T_{j}) ⇒ □Inv.1

⟨2⟩3. Π^{t} ⇒ □Inv.3

⟨2⟩4. Π^{t} ⇒ □Inv.4

⟨2⟩5. Π^{t} ⇒ □Inv.5

⟨2⟩6. Q.E.D.

Proof: ⟨2⟩1–⟨2⟩5. ⟨1⟩3. 1. Π = Init ∧ □M

2. Π^{t} = Init^{t} ∧ □N^{t}, for some predicate Init^{t}.

where

M =^{Δ} ∧ [N]_{w} ∧ ∀j ∈ J_{P} : PTact(T_{j}, A_{j}, Δ_{j}, v) ∧ ∀j ∈ J_{V} : VTact(T_{j}, A_{j}, Δ_{j}, v)

N^{t} =^{Δ} ∧ M ∧ RTact_{v} ∧ ∀i ∈ I : MinTact(t_{i}, A_{i}, v) ∧ ∀j ∈ J : MaxTact(T_{j})

Proof: 1 follows from assumptions ⟨0⟩.0a and ⟨0⟩.3b, and 2 follows from the definition of Π^{t}, since □ distributes over ∧. (A simple calculation shows that M = [M]_{f} and N^{t} = [N^{t}]_{g}, for suitable tuples f and g, so □M and □N^{t} are TLA formulas.)

⟨1⟩4. ⟨C⟩_{(now,v)} is a subaction of Π^{t}. ⟨2⟩1. For all j in J : ⟨B_{j}^{t}⟩_{v} is a subaction of Π^{t}. ⟨2⟩2. ⟨NowT ⟩_{now} is a subaction of Π^{t}. ⟨2⟩3. Q.E.D.

Proof: By ⟨2⟩1 and ⟨2⟩2, since ⟨NowT ⟩_{now} = ⟨NowT ⟩_{(now,v)}, ⟨B_{j}^{t}⟩_{v} = ⟨B_{j}^{t}⟩_{(now,v)}, Lemma 4.4 implies that the disjunction of subactions is a subaction, and Lemma 4.3 implies that if D is a subaction, then P ∧ D is also a subaction, for any predicate P.

⟨1⟩5. Π^{t} ∧ WF_{(now,v)}(C) ⇒ NZ Proof: By the Lattice Rule [Lamport 1991], it suffices to Assume: r ∈ R Prove: Π^{t} ∧ WF_{(now,v)}(C) ⇒ ( (now = r) ⇝ (now ∈ [[r + Δ, ∞))) ) Proof sketch: The standard method of proving that now = r leads to now ∈ [[r + Δ, ∞)) is to assume that now = r and now is never in [[r + Δ, ∞)), and derive a contradiction. Step ⟨2⟩2 below proves that, if now equals r and it is never in [[r + Δ, ∞)), then it is always in [[r, r + Δ)). It therefore suffices to assume now is always in [[r, r + Δ)) and derive the contradiction. The contradiction is obtained by showing that eventually there is no upper-bound timer preventing the advance of now past r + Δ. The timers that could prevent the advance of now are the ones in the set U of timers that are less than r + Δ. Step ⟨2⟩4 asserts that U eventually becomes empty, and ⟨2⟩5 asserts that time then advances past r + Δ.

Let: U =^{Δ} {j ∈ J : T_{j} < r + Δ}

V =^{Δ} {j ∈ J : now < T_{j} < r + Δ}

TimerAct =^{Δ} ∀j ∈ J : ∨ VTact(T_{j}, A_{j}, Δ_{j}, v) ∨ PTact(T_{j}, A_{j}, Δ_{j}, v)

⟨2⟩1. Inv ⇒ Enabled ⟨C⟩_{(now,v)}

⟨2⟩2. Π^{t} ⇒

□((now = r) ∧ □(now ∈ (( − ∞, r + Δ))) ⇒ □(now ∈ [[r, r + Δ))))

⟨2⟩3. Assume: j ∈ J

Prove: 1. Π^{t} ∧ □(now ∈ [[r, r + Δ))) ⇒ □((j ∉ U) ⇒ □(j ∉ U))

2. Π^{t} ∧ □(now ∈ [[r, r + Δ))) ⇒ □((j ∉ V) ⇒ □(j ∉ V))

⟨2⟩4. Π^{t} ∧ □(now ∈ [[r, r + Δ))) ∧ WF_{(now,v)}(C) ⇒ ◇□(U = ∅)

⟨2⟩5. ∧ □(now ∈ [[r, r + Δ)))

∧ □(U = ∅) ∧ □Inv ∧ WF_{(now,v)}(C) ⇒ true ⇝ (now ≥ r + Δ)

⟨2⟩6. Q.E.D.

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

Proof: ⟨2⟩2, ⟨2⟩4, ⟨2⟩5, ⟨1⟩2, and temporal logic. ⟨1⟩6. (E −▷ M^{t}, E ⇒ WF_{(now,v)}(C)) is μ-machine realizable.

⟨2⟩1. M^{t} constrains at most μ. ⟨2⟩2. Q.E.D.

Proof: We apply Proposition 4, with E substituted for Φ, M^{t} substituted for Π, and the single formula WF_{(now,v)}(C). Step ⟨2⟩1 asserts that M^{t} constrains at most μ. The three numbered hypotheses of the proposition are proved as follows:

1. ⟨1⟩4.

2. Assumptions ⟨0⟩.5a and ⟨0⟩.5b and the definition of C.

3. Vacuous. ⟨1⟩7. (true, NZ ) is μ-machine realizable.

Proof: Assumption ⟨0⟩.5b. ⟨1⟩8. Q.E.D.

Proof: Proposition 5, using ⟨0⟩.4, ⟨1⟩6, ⟨1⟩7, and ⟨1⟩5.

B7.2 Detailed Proof of the Theorem ⟨1⟩1. Choose J_{P} and J_{V} such that:

1. J = J_{P} ∪ J_{V}

2. J_{P} ∩ J_{V} = ∅

3. ∀j ∈ J_{V} : Π ⇒ VTimer(T_{j}, A_{j}, Δ_{j}, v)

4. ∀j ∈ J_{P} : Π ⇒ P T imer(T_{j}, A_{j}, Δ_{j}, v)

⟨1⟩2. Π^{t} ⇒ □Inv, where Inv =^{Δ} 1.∧ ∀j ∈ J : T_{j} ∈ [[now, ∞]] 2.∧ now ∈ R 3.∧ ∀j ∈ J : (Enabled ⟨A_{j}⟩_{v} = Enabled (⟨A_{j}⟩_{v} ∧ (now′ = now)) 4.∧ ∀k ∈ I ∩ J : t_{k} ≤ T_{k} 5.∧ ∀j ∈ J_{V} : ¬Enabled ⟨A_{j}⟩_{v} ⇒ (T_{j} = ∞)

⟨2⟩1. RT_{v} ⇒ □Inv.2

Proof: An invariance proof. ⟨2⟩2. For all j ∈ J : Π ∧ □Inv.2 ∧ MaxTime(T_{j}) ⇒ □Inv.1

Proof: Assumption ⟨0⟩.0c and an invariance proof. ⟨2⟩3. Π^{t} ⇒ □Inv.3

Proof: Assumption ⟨0⟩.3c. ⟨2⟩4. Π^{t} ⇒ □Inv.4

Proof: Assumption ⟨0⟩.1. ⟨2⟩5. Π^{t} ⇒ □Inv.5

Proof: ⟨1⟩1.3, assumption ⟨0⟩.3d, and an invariance proof. ⟨2⟩6. Q.E.D.

⟨1⟩3. 1. Π = Init ∧ □M

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

2. Π^{t} = Init^{t} ∧ □N^{t}, for some predicate Init^{t}. where

M =^{Δ} ∧ [N]_{w} ∧ ∀j ∈ J_{P} : PTact(T_{j}, A_{j}, Δ_{j}, v) ∧ ∀j ∈ J_{V} : VTact(T_{j}, A_{j}, Δ_{j}, v)

N^{t} =^{Δ} ∧ M ∧ RTact_{v} ∧ ∀i ∈ I : MinTact(t_{i}, A_{i}, v) ∧ ∀j ∈ J : MaxTact(T_{j})

⟨1⟩4. ⟨C⟩_{(now,v)} is a subaction of Π^{t}.

⟨2⟩1. For all j in J : ⟨B_{j}^{t}⟩_{v} is a subaction of Π^{t}. Assume: j ∈ J Prove: Π^{t} ⇒ □ ( Enabled ⟨B_{j}^{t}⟩_{v} ⇒ Enabled (⟨B_{j}^{t}⟩_{v} ∧ N^{t}) )

⟨3⟩1. Π^{t} ⇒ □ (\begin{matrix}Enabled (⟨B_{j}^{t}⟩_{v} ∧ M) ⇒ \\ Enabled (\begin{matrix}∧ ⟨B_{j}^{t}⟩_{v} ∧ M \\ ∧ ∀i ∈ I − \{j\} : ¬(⟨A_{i}⟩_{v} ∧ ⟨A_{j}⟩_{v} ∧ M) ∨ (t_{i} ≤ T_{j}) ) ) \end{matrix} \end{matrix}

⟨4⟩1. Π^{t} ⇒ ¬Enabled (∃ i ∈ I − {j} : (⟨A_{i}⟩_{v} ∧ ⟨A_{j}⟩_{v} ∧ M) ∧ ¬(t_{i} ≤ T_{j}))

Proof: ⟨1⟩3.1, assumption ⟨0⟩.1, Lemma 4.3, and Lemma 4.4. ⟨4⟩2. Q.E.D.

Proof: Lemma 4.2, substituting ⟨B_{j}^{t}⟩_{v} ∧ M for A and ∃ i ∈ I − {j} : (⟨A_{i}⟩_{v} ∧ ⟨A_{j}⟩_{v} ∧ M) ∧ ¬(t_{i} ≤ T_{j}) for B.

⟨3⟩2. \begin{matrix}∧ ⟨B_{j}^{t}⟩_{v} ∧ N^{t} \\ ∧ ∀i ∈ I − \{j\} : ¬(⟨A_{i}⟩_{v} ∧ ⟨A_{j}⟩_{v} ∧ M) ∨ (t_{i} ≤ T_{j}) \end{matrix}

= \begin{matrix}∧ ⟨B_{j}^{t}⟩_{v} ∧ M \\ ∧ ∀i ∈ I − \{j\} : ¬(⟨A_{i}⟩_{v} ∧ ⟨A_{j}⟩_{v} ∧ M) ∨ (t_{i} ≤ T_{j}) \end{matrix}

Proof: \begin{matrix}∧ ⟨B_{j}^{t}⟩_{v} ∧ N^{t} \\ ∧ ∀i ∈ I − \{j\} : ¬(⟨A_{i}⟩_{v} ∧ ⟨A_{j}⟩_{v} ∧ M) ∨ (t_{i} ≤ T_{j}) \end{matrix}

= [by definition of ⟨B_{j}^{t}⟩_{v}] ∧ A_{j}^{t} ∧ (v′ ≠ v) ∧ (now′ = now) ∧ (T_{j} = now) ∧ N^{t} ∧ ∀i ∈ I − {j} : ¬(⟨A_{i}⟩_{v} ∧ ⟨A_{j}⟩_{v} ∧ M) ∨ (t_{i} ≤ T_{j})

= [by definition of N^{t}] ∧ A_{j}^{t} ∧ M ∧ (v′ ≠ v) ∧ (now′ = now) ∧ (T_{j} = now) ∧ ∀i ∈ I : A_{i} ⇒ (t_{i} ≤ now) ∧ ∀i ∈ I − {j} : ¬(⟨A_{i}⟩_{v} ∧ ⟨A_{j}⟩_{v} ∧ M) ∨ (t_{i} ≤ T_{j})

= [by definition of A_{j}^{t}] ∧ P_{j} ∧ A_{j} ∧ M ∧ (v′ ≠ v) ∧ (now′ = now) ∧ (T_{j} = now) ∧ ∀i ∈ I : A_{i} ⇒ (t_{i} ≤ now) ∧ ∀i ∈ I − {j} : ¬(A_{i} ∧ A_{j} ∧ M ∧ (v′ ≠ v)) ∨ (t_{i} ≤ T_{j})

= [by predicate logic] ∧ P_{j} ∧ A_{j} ∧ M ∧ (v′ ≠ v) ∧ (now′ = now) ∧ (T_{j} = now) ∧ (j ∈ I) ⇒ (t_{j} ≤ now) ∧ ∀i ∈ I − {j} : ¬(A_{i} ∧ A_{j} ∧ M ∧ (v′ ≠ v)) ∨ (t_{i} ≤ T_{j})

= [by definition of ⟨A_{k}⟩_{v}] ∧ P_{j} ∧ A_{j} ∧ M ∧ (v′ ≠ v) ∧ (now′ = now) ∧ (T_{j} = now) ∧ (j ∈ I) ⇒ (t_{j} ≤ now) ∧ ∀i ∈ I − {j} : ¬(⟨A_{i}⟩_{v} ∧ ⟨A_{j}⟩_{v} ∧ M) ∨ (t_{i} ≤ T_{j})

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

= [by definition of P_{j}] ∧ P_{j} ∧ A_{j} ∧ (v′ ≠ v) ∧ (now′ = now) ∧ (T_{j} = now) ∧ M ∧ ∀i ∈ I − {j} : ¬(⟨A_{i}⟩_{v} ∧ ⟨A_{j}⟩_{v} ∧ M) ∨ (t_{i} ≤ T_{j})

= [by definition of ⟨B_{j}^{t}⟩_{v}]

\begin{matrix}∧ ⟨B_{j}^{t}⟩_{v} ∧ M \\ ∧ ∀i ∈ I − \{j\} : ¬(⟨A_{i}⟩_{v} ∧ ⟨A_{j}⟩_{v} ∧ M) ∨ (t_{i} ≤ T_{j}) \end{matrix}

⟨3⟩3. Π^{t} ⇒ □ ( Enabled (⟨B_{j}^{t}⟩_{v} ∧ M) ⇒ Enabled (⟨B_{j}^{t}⟩_{v} ∧ N^{t}) )

Proof: ⟨3⟩1, ⟨3⟩2, and Lemma 4.5. ⟨3⟩4. Π^{t} ⇒ □(P_{j} ∧ (T_{j} = now) ∧ Enabled ⟨B_{j}⟩_{v} ⇒ P_{j} ∧ (T_{j} = now) ∧

Enabled (⟨B_{j}⟩_{v} ∧ M)) Proof: ⟨1⟩3, Assumption ⟨0⟩.3a, and the definition of B_{j}.

⟨3⟩5. Π^{t} ⇒ □ ( (Enabled ⟨B_{j}^{t}⟩_{v}) ⇒ Enabled (⟨B_{j}^{t}⟩_{v} ∧ M) )

Proof: ⟨3⟩4, the definition of B_{j}^{t}, and Lemma 4.3. ⟨3⟩6. Q.E.D.

Proof: ⟨3⟩5 and ⟨3⟩3. ⟨2⟩2. ⟨NowT ⟩_{now} is a subaction of Π^{t}.

⟨3⟩1. Π^{t} ⇒ □ ( \begin{matrix}(Enabled ⟨NowT ⟩_{now}) ⇒ \\ (Enabled (⟨NowT ⟩_{now} ∧ M)) ) \end{matrix}

⟨4⟩1. Π^{t} ⇒ □ ( (Enabled NowT ) ⇒ (Enabled (NowT ∧ M)) ) Proof: ⟨1⟩3, assumption ⟨0⟩.2b, and the definition of NowT , since Π^{t} implies Π.

⟨4⟩2. Q.E.D.

Proof: ⟨4⟩1 and Lemma 4.3, substituting now ≠ T for P (since ⟨NowT ⟩_{now} equals NowT ∧ (now ≠ T)).

⟨3⟩2. Π^{t} ⇒ □(\begin{matrix}Enabled (⟨NowT ⟩_{now} ∧ M) ⇒ \\ Enabled (⟨NowT ⟩_{now} ∧ N^{t})) \end{matrix}

⟨4⟩1. (Inv ∧ ⟨NowT ⟩_{now} ∧ M) ⇒ (⟨NowT ⟩_{now} ∧ N^{t})

⟨5⟩1. Inv ∧ ⟨NowT ⟩_{now} ⇒ RTact_{v}

Proof: ⟨1⟩3 (Inv.1 and Inv.2). ⟨5⟩2. ∀i ∈ I : ⟨NowT ⟩_{now} ⇒ MinTact(t_{i}, A_{i}, v)

Proof: MinTact(t_{i}, A_{i}, v) = [ …]_{v}, and ⟨NowT ⟩_{now} implies v′ = v. ⟨5⟩3. ∀j ∈ J : Inv ∧ ⟨NowT ⟩_{now} ∧ M ⇒ MaxTact(T_{j}) Assume: 1. j ∈ J

2. Inv ∧ ⟨NowT ⟩_{now} ∧ M

Prove: MaxTact(T_{j})

⟨6⟩1. Case: Enabled ⟨A_{j}⟩_{v}

⟨7⟩1. now′ ≤ T_{j} Proof: Inv.1, Inv.2, ⟨NowT ⟩_{now}, and the definitions of NowT , since case assumption ⟨6⟩ and the definition of T imply T_{j} ≥ T.

⟨7⟩2. Case: j ∈ J_{P}

⟨8⟩1. Case: T′_{j} = T_{j}

Proof: ⟨7⟩1 and the definition of MaxTact(T_{j}). ⟨8⟩2. Case: T′_{j} = now + Δ_{j}

Proof: Inv.2, ⟨NowT ⟩_{now}, and definition of MaxTact(T_{j}). ⟨8⟩3. Q.E.D.

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

Proof: ⟨8⟩1, ⟨8⟩2, and case assumption ⟨7⟩, since case assumption ⟨6⟩ and the definition of PTact(T_{j}, A_{j}, Δ_{j}, v) imply that these are the only possibilities.

⟨7⟩3. Case: j ∈ J_{V}

⟨8⟩1. T_{j} = T′_{j} Proof: Case assumption ⟨7⟩ and the definitions of M and VTact(T_{j}, A_{j}, Δ_{j}, v), since ⟨NowT ⟩_{v} implies v = v′.

⟨8⟩2. Q.E.D.

Proof: ⟨7⟩1, ⟨8⟩1, and the definition of MaxTact(T_{j}). ⟨7⟩4. Q.E.D.

Proof: ⟨7⟩2, ⟨7⟩3, ⟨1⟩1.1, and assumption ⟨5⟩.1. ⟨6⟩2. Case: ¬Enabled ⟨A_{j}⟩_{v}

⟨7⟩1. now, now′ ∈ R and now′ > now.

Proof: Inv.1, Inv.2, ⟨NowT ⟩_{now}, and the definition of T. ⟨7⟩2. Case: j ∈ J_{P}

⟨8⟩1. T′_{j} ≥ now′ Proof: ⟨7⟩1, case assumption ⟨7⟩, Inv.1, and the definitions of M and PTact(T_{j}, A_{j}, Δ_{j}, v).

⟨8⟩2. Q.E.D.

Proof: ⟨8⟩1 and the definition of MaxTact(T_{j}). ⟨7⟩3. Case: j ∈ J_{V}

⟨8⟩1. T_{j} = ∞

Proof: By case assumption ⟨7⟩ and Inv.5. ⟨8⟩2. T′_{j} = ∞

Proof: ⟨8⟩1, case assumption ⟨7⟩, and the definitions of M and VTact(T_{j}, A_{j}, Δ_{j}, v), since ⟨NowT ⟩_{v} implies v = v′.

⟨8⟩3. Q.E.D.

Proof: ⟨7⟩1, ⟨8⟩2, and the definition of MaxTact(T_{j}). ⟨7⟩4. Q.E.D.

Proof: ⟨7⟩2, ⟨7⟩3, ⟨1⟩1.1, and assumption ⟨5⟩.1. ⟨6⟩3. Q.E.D.

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

Proof: ⟨5⟩1, ⟨5⟩2, ⟨5⟩3, and the definition of N^{t}. ⟨4⟩2. Q.E.D.

Proof: ⟨4⟩1 and ⟨1⟩2, since by Lemma 4.3 and Lemma 4.5, Inv ∧ D ⇒ E implies □Inv ⇒ □((Enabled D) ⇒ (Enabled E)), for any actions D and E.

⟨3⟩3. Q.E.D.

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

⟨1⟩5. Π^{t} ∧ WF_{(now,v)}(C) ⇒ NZ Assume: r ∈ R Prove: Π^{t} ∧ WF_{(now,v)}(C) ⇒ ( (now = r) ⇝ (now ∈ [[r + Δ, ∞))) )

Let: U =^{Δ} {j ∈ J : T_{j} < r + Δ}

V =^{Δ} {j ∈ J : now < T_{j} < r + Δ}

TimerAct =^{Δ} ∀j ∈ J : ∨ VTact(T_{j}, A_{j}, Δ_{j}, v) ∨ PTact(T_{j}, A_{j}, Δ_{j}, v)

⟨2⟩1. Inv ⇒ Enabled ⟨C⟩_{(now,v)}

⟨3⟩1. Case: T ≠ now Proof: By the definition of C, since case assumption ⟨3⟩ implies Enabled ⟨NowT ⟩_{now}.

⟨3⟩2. Case: T = now

⟨4⟩1. Choose j ∈ J such that (T_{j} = T) ∧ Enabled ⟨A_{j}⟩_{v}.

Proof: Inv.2, case assumption ⟨3⟩, and the definition of T. ⟨4⟩2. (T_{j} = T) ∧ Enabled ⟨B_{j}⟩_{v}

Proof: ⟨4⟩1, Inv.3, and the definition of ⟨B_{j}⟩_{v}. ⟨4⟩3. Enabled ⟨B_{j}^{t}⟩_{v}

Proof: ⟨4⟩2, Inv.4, case assumption ⟨3⟩, and the definition of ⟨B_{j}^{t}⟩_{v}. ⟨4⟩4. Q.E.D.

Proof: Case assumption ⟨3⟩, ⟨4⟩3, and the definition of C. ⟨3⟩3. Q.E.D.

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

⟨2⟩2. Π^{t} ⇒

□((now = r) ∧ □(now ∈ (( − ∞, r + Δ))) ⇒ □(now ∈ [[r, r + Δ))))

⟨3⟩1. □[RTact_{v}]_{now} ⇒ ((now = r) ⇒ □(now ∈ [[r, ∞))))

Proof: A standard invariance argument. ⟨3⟩2. □[RTact_{v}]_{now} ⇒ □((now = r) ⇒ □(now ∈ [[r, ∞))))

Proof: ⟨3⟩1 and simple temporal logic. ⟨3⟩3. Π^{t} ⇒ □((now = r) ⇒ □(r ≤ now))

Proof: ⟨3⟩2, since Π^{t} ⇒ RT_{v} and RT_{v} ⇒ □[RTact_{v}]_{now}. ⟨3⟩4. Q.E.D.

Proof: ⟨3⟩3, using the temporal logic tautology

(F ⇝ G) ⇒ ((F ∧ □H) ⇝ (G ∧ □H))

⟨2⟩3. Assume: j ∈ J

Prove: 1. Π^{t} ∧ □(now ∈ [[r, r + Δ))) ⇒ □((j ∉ U) ⇒ □(j ∉ U))

2. Π^{t} ∧ □(now ∈ [[r, r + Δ))) ⇒ □((j ∉ V) ⇒ □(j ∉ V))

Proof: A standard invariance proof, using assumption ⟨0⟩.3b. ⟨2⟩4. Π^{t} ∧ □(now ∈ [[r, r + Δ))) ∧ WF_{(now,v)}(C) ⇒ ◇□(U = ∅)

Proof sketch: The set V consists of those timers in U that are not equal to now. To prove that U is eventually empty, we show that, whenever U is nonempty, eventually U or V gets smaller. Since U and V are finite, U must eventually become empty. ⟨3⟩1. Assume: U_{0} and V_{0} sets, with U_{0} ≠ ∅.

Prove: ∧ □((U ⊆ U_{0}) ∧ (V ⊆ V_{0}))

∧ □(now ∈ [[r, r + Δ)))
∧ □Inv
∧ □[TimerAct]_{(now,v)}
∧ WF_{(now,v)}(C)
⇒ ((U = U_{0}) ∧ (V = V_{0})) ⇝
(U ⊂ U_{0}) ∨ ((U ⊆ U_{0}) ∧ (V ⊂ V_{0}))

Proof sketch: This is a straightforward application of rule WF1 (Lemma 3), with the following substitutions.

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

Let: I =^{Δ} \begin{matrix}1.∧ now ∈ [[r, r + Δ)) \\ 2.∧ (U ⊆ U_{0}) ∧ (V ⊆ V_{0}) \\ 3.∧ Inv \end{matrix}

P =^{Δ} (U = U_{0}) ∧ (V = V_{0})

Q =^{Δ} (U ⊂ U_{0}) ∨ ((U ⊆ U_{0}) ∧ (V ⊂ V_{0}))

N =^{Δ} TimerAct

A =^{Δ} C

f =^{Δ} (now, v)

⟨4⟩1. I′ ⇒ (P′ ∨ Q′)

Proof: Obvious. ⟨4⟩2. Assume: P ∧ I ∧ I′ ∧ ⟨N ∧ A⟩_{f}

Prove: Q′ ⟨5⟩1. Case: T = now

⟨6⟩1. Choose j in J such that (T_{j} = T) ∧ ⟨B_{j}^{t}⟩_{v}.

Proof: A (from case assumption ⟨4⟩) and case assumption ⟨5⟩. ⟨6⟩2. T′_{j} ≥ r + Δ

Proof: ⟨6⟩1, I.1, the definition of B_{j}^{t}, and TimerAct. ⟨6⟩3. j ∈ U ∧ j ∉ U′

Proof: ⟨6⟩1, case assumption ⟨5⟩, and I.1. ⟨6⟩4. j ∉ U′

Proof: ⟨6⟩2. ⟨6⟩5. Q.E.D.

Proof: ⟨6⟩3, ⟨6⟩4, and I′.2. ⟨5⟩2. Case: T ≠ now

⟨6⟩1. (now′ = T) ∧ (v′ = v)

Proof: A and case assumption ⟨5⟩. ⟨6⟩2. Case: T ∈ (now, r + Δ)

⟨7⟩1. Choose j in J such that (T_{j} = T) ∧ Enabled ⟨A⟩_{v}.

Proof: Case assumption ⟨6⟩ and the definition of T.

⟨7⟩2. \begin{matrix}∨ T′_{j} = now′ \\ ∨ T′_{j} ∈ [[r + Δ, ∞]] \end{matrix}

Proof: ⟨6⟩1, ⟨7⟩1, I.1, and TimerAct. ⟨7⟩3. j ∈ V

Proof: ⟨7⟩1, case assumption ⟨6⟩, and the definition of V. ⟨7⟩4. j ∉ V′

Proof: ⟨7⟩2 and the definition of V. ⟨7⟩5. Q.E.D.

⟨7⟩3, ⟨7⟩4, and I′.2. ⟨6⟩3. Case: T ∈ [[r + Δ, ∞]]

Proof: Impossible by ⟨6⟩1 and I′.1. ⟨6⟩4. Q.E.D.

Proof: ⟨6⟩2, ⟨6⟩3, I.3.1, and case assumption ⟨5⟩. ⟨5⟩3. Q.E.D.

Proof: ⟨5⟩1 and ⟨5⟩2. ⟨4⟩3. P ∧ I ⇒ Enabled ⟨A⟩_{f}

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

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

Proof: ⟨4⟩1, ⟨4⟩2, ⟨4⟩3, and Lemma 3. ⟨3⟩2. Assume: U_{0} and V_{0} sets, with U_{0} ≠ ∅.

Prove: Π^{t} ∧ □(now ∈ [[r, r + Δ))) ∧ WF_{(now,v)}(C) ⇒

((U = U_{0}) ∧ (V = V_{0})) ⇝

((U ⊂ U_{0}) ∨ ((U ⊆ U_{0}) ∧ (V ⊂ V_{0})))

⟨4⟩1. Π^{t} ⇒ □((U ⊆ U_{0}) ∧ (V ⊆ V_{0}) ⇒ □((U ⊆ U_{0}) ∧ (V ⊆ V_{0})))

Proof: Follows from ⟨2⟩3. ⟨4⟩2. Q.E.D.

Proof: ⟨3⟩1, ⟨4⟩1, and ⟨1⟩2, since Π^{t} ⇒ □[TimerAct]_{(now,v)} by assumption ⟨0⟩.3b.

⟨3⟩3. Q.E.D.

Proof: Since U and V are finite by assumption ⟨0⟩.0d, it follows from ⟨3⟩2 and the Lattice Rule [Lamport 1991] that Π^{t} ∧ □(now ∈ [[r, r + Δ))) ∧ WF_{(now,v)}(C) implies ◇(U = ∅). By ⟨2⟩3, Π^{t} ∧ □(now ∈ [[r, r + Δ))) implies ◇(U = ∅) ⇒ ◇□(U = ∅).

⟨2⟩5. ∧ □(now ∈ [[r, r + Δ)))

∧ □(U = ∅) ∧ □Inv ∧ WF_{(now,v)}(C) ⇒ true ⇝ (now ≥ r + Δ)

Let: I =^{Δ} \begin{matrix}1.∧ U = ∅ \\ 2.∧ now ∈ [[r, r + Δ)) \\ 3.∧ Inv \end{matrix}

P =^{Δ} true

Q =^{Δ} now ≥ r + Δ

N =^{Δ} true

A =^{Δ} C

f =^{Δ} (now, v)

⟨3⟩1. I ∧ I′ ∧ [N]_{f} ⇒ (P′ ∨ Q′)

Proof: Immediate, since P′ = true. ⟨3⟩2. Assume: P ∧ I ∧ I′ ∧ ⟨N ∧ A⟩_{f}

Prove: Q′ ⟨4⟩1. T ∈ [[r + Δ, ∞]]

Proof: By I. ⟨4⟩2. ⟨NowT ⟩_{now}

Proof: By ⟨4⟩1, I.2, and A. ⟨4⟩3. Q.E.D.

Proof: ⟨4⟩1, ⟨4⟩2, and the definition of NowT . ⟨3⟩3. P ∧ I ⇒ Enabled ⟨A⟩_{f}

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

Proof: ⟨3⟩1, ⟨3⟩2, ⟨3⟩3, and Lemma 3. ⟨2⟩6. Q.E.D.

⟨1⟩6. (E −▷ M^{t}, E ⇒ WF_{(now,v)}(C)) is μ-machine realizable.

⟨2⟩1. M^{t} constrains at most μ.

⟨3⟩1. M constrains at most μ.

Proof: Assumption ⟨0⟩.4.

ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.

⟨3⟩2. RT_{v} constrains at most μ.

Proof: Assumption ⟨0⟩.5b. ⟨3⟩3. For all i in I, MinTime(t_{i}, A_{i}, v) constrains at most μ.

Proof: By definition of MinTime, a step violates MinTime(t_{i}, A_{i}, v) only if it is an ⟨A_{i}⟩_{v} step, so this follows from Assumption ⟨0⟩.5a.

⟨3⟩4. For all j in J, MaxTime(T_{j}) constrains at most μ.

Proof: Assumption ⟨0⟩.5b. ⟨3⟩5. Q.E.D.

Proof: ⟨3⟩1–⟨3⟩4 and the definition of M^{t}. ⟨2⟩2. Q.E.D.

⟨1⟩7. (true, NZ ) is μ-machine realizable. ⟨1⟩8. Q.E.D.

Received November 1992; revised November 1993; accepted ???.