Verifying Clocked Transition Systems^{⋆}

Yonit Kesten^{†} Zohar Manna^{‡} Amir Pnueli^{†}

Abstract. This paper presents a new computational model for realtime systems, called the clocked transition system model. The model is a development of our previous timed transition model, where some of the changes are inspired by the model of timed automata. The new model leads to a simpler style of temporal specification and verification, requiring no extension of the temporal language. For verifying safety properties, we present a run-preserving reduction from the new real-time model to the untimed model of fair transition systems. This reduction allows the (re)use of safety verification methods and tools, developed for untimed reactive systems, for proving safety properties of real-time systems.

1 Introduction

A formal framework for specifying and verifying temporal properties of reactive systems often contains the following components:

• A computational model defining the set of behaviors (computations) that are to be associated with systems in the considered model.

• A requirement specification language for specifying properties of systems within the model. The languages we have considered in our previous work are all variants of temporal logic extended to deal with various aspects specific to the considered model, such as real-time and continuously changing variables.

• A system description language for describing systems within the model. We frequently use both a textual programming language and appropriate extensions of the graphical language of statecharts [Har87] to present systems.

• A set of proof rules by which valid properties of systems can be verified, showing that the systems satisfy their specifications.

• A set of algorithmic methods enabling a fully automatic verification of decidable subclasses of the verification problem such as the verification of finitestate systems (model checking).

⋆ This research was supported in part by the National Science Foundation under grant CCR-92-23226, by the Advanced Research Projects Agency under NASA grant NAG2-892, by the United States Air Force Office of Scientific Research under grant F49620-93-1-0139, and by Department of the Army under grant DAAH04-95-1-0317, by a basic research grant from the Israeli Academy of Sciences, and by the European Community ESPRIT Basic Research Action Project 6021 (REACT). † Department of Computer Science, Weizmann Institute, Rehovot, Israel, e-mail:

yonit@wisdom.weizmann.ac.il

‡ Department of Computer Science, Stanford University, Stanford, CA 94305, e-mail:

manna@cs.stanford.edu

In [MP93], we considered a hierarchy of three models, each extending its predecessor, as follows:

• A reactive systems model that captures the qualitative (non-quantitative) temporal precedence aspect of time. This model can only identify that one event precedes another but not by how much.

• A real-time systems model that captures the metric aspect of time in a reactive system. This model can measure the time elapsing between two events.

• A hybrid systems model that allows the inclusion of continuous components in a reactive real-time system. Such continuous components may cause continuous change in the values of some state variables according to some physical or control law.

The computational model proposed for reactive systems is that of a fair transition system (fts) [MP91b].

The approach to real time presented in [MP93] and [HMP94] is based on the computational model of timed transition systems (tts) in which time itself is not explicitly represented but is reflected in a time stamp affixed to each state in a computation of a tts. As a result of time not being available as a value of some variable, the requirement specification language must be based on a necessary extension of temporal logic. In [MP93], we present two such extensions: metric temporal logic (mtl) which introduces bounded versions of the temporal operators, subscripted by an interval specification, and temporal logic with age (TL_{Γ}) which introduces the operator Γ, measuring the length of recent time in which a certain formula held continuously.

Consider, for example, the following important timed properties:

• Bounded response: Every p should be followed by an occurrence of a q, not later than d time units.

• Minimal separation: No q can occur earlier than d time units after an occurrence of p.

In mtl, these two properties can be specified as follows:

• Bounded response: p =≻ � _{≤d} q.
• Minimal separation: p =≻ � _{<d} ¬q.

This approach to the specification of timing properties has been advocated in [KVdR83], [KdR85], and [Koy90], although an early proposal in [BH81] can be viewed as a precursor to this specification style. Using TL_{Γ}, the same properties can be specified by:

• Bounded response: � [Γ ((¬q) S(p ∧ ¬q)) ≤ d].
• Minimal separation: q =≻ (� (¬p) ∨ Γ (¬p) ≥ d).

When constructing detailed proofs of such timed properties, we found it necessary to form many auxiliary invariants involving the age function Γ. Very soon, we realized that each age expression of the form Γ (p) represents a timer that started measuring time as soon as p becomes true and is reset (or shut off) whenever p becomes false. This led to the suggestion that age expressions can be eliminated in favor of the introduction of explicit timers.

Meanwhile, the model of timed automata [AD94] has gained dominance in the arena of real-time algorithmic verification. This model uses timers which can only be reset by system transitions but increase uniformly whenever time progresses. However, aiming at algorithmic verification, this model can only capture finitestate systems.

In this paper we present a new computational model for real-time systems: clocked transition system (cts). This model represents time by a set of clocks (timers) which increase uniformly whenever time progresses, but can be set to arbitrary values by system (program) transitions.

It is easy and natural to stipulate that one of the clocks T is never reset. In this case, T represents the master clock measuring real time from the beginning of the computation. This immediately yields the possibility of specifying timing properties of systems by unextended temporal logic, which may refer to any of the system variables, including the master clock T. Thus, the two yardstick properties considered above can be specified by the following (unextended) temporal formulas:

• Bounded response: p ∧ (T = t_{0}) =≻ � (q ∧ T ≤ t_{0} + d).
• Minimal separation: p ∧ (T = t_{0}) =≻ � (T < t_{0} + d → ¬q).

A first advantage of the new computational model over its predecessors is that it leads to a more natural style of verification proofs, stating invariants in terms of clocks, which are just another kind of system variables, instead of formulating invariants in terms of Γ -expressions. A second advantage is that we can use temporal logic without any extensions as the specification language, and can reuse many of the methods and tools developed for verifying reactive systems, under the fts computational model, for verifying real-time systems under the cts model. Another advantage of the cts model is that it can be viewed as a natural first-order extension of the timed automata model [AD94].

In order to reuse fts verification methods for verifying cts properties, we will show that for every cts Φ there exists a corresponding fts P_{Φ} such that the runs of Φ and the runs of P_{Φ} coincide. It follows that any safety property is valid over the cts Φ iff it is valid over the fts P_{Φ}. This reduction from real-time systems to simpler transition systems enables us to use the deductive methodology developed for proving safety properties of reactive systems, as well as support systems for this methodology such as [MAB^{+}94], for establishing safety properties of timed systems.

It is interesting to note that the move from tts to cts brings us closer to the approach proposed in [AL94], which also recommends handling real time with a minimal extension of the reactive-systems formalism.

The restriction to safety properties is not as constraining as one may think. Many properties whose untimed version falls into the liveness class become safety properties when we consider their timed version. For example, termination of a program is a liveness property. However, the property of termination within 15 time units is a safety property. This indicates that, when we move to realtime systems, the set of safety properties we may want to prove constitutes an even higher portion of the total set of properties of interest than in the case of untimed reactive-systems. We refer the reader to [Hen92] and [Pnu92] for further discussions of this point.

refer to the two Hen- We refer the reader to [AH89], [Ost90], [AL94], and the survey in [AH92], for zinger’s papers additional logics, models, and approaches to the verification of real-time systems.

In the process algebra school, some of the representative approaches to real time are [NSY92], [MT90], and many others are listed in [Sif91].

The paper is organized as follows. In Section 2, we present the real-time computational model of clocked transition systems (cts). In Section 3, we show how programs augmented with timing bounds for the execution of statements can be represented as clocked transition systems. In Section 4, we present rules and verification diagrams for verifying safety properties of cts’s. In Section 5, we present rules and verification diagrams for establishing response properties of clocked transition systems. Finally, in Section 6, we present an approach to verifying that a given cts is non-zeno.

2 Real-Time Systems

We now introduce a computational model for real-time systems.

2.1 Computational Model: Clocked Transition System

Real-time systems are modeled as clocked transition systems (cts). A clocked transition system Φ = ⟨V, Θ, T , Π⟩ consists of:

• V = {u_{1}, …, u_{n}} : A finite set of system variables. The set V = D ∪ C is partitioned into D the set of discrete variables and C the set of clocks. Clocks always have the type real. The discrete variables can be of any type. We introduce a special clock T ∈ C, representing the master clock, as one of the system variables.

• Θ : The initial condition. A satisfiable assertion characterizing the initial states. It is required that

Θ → T = 0,

i.e., T = 0 at all initial states.

• T : A finite set of transitions. Each transition τ ∈ T is a function

τ : Σ ↦ 2^{Σ},

mapping each state s ∈ Σ into a (possibly empty) set of τ-successor states τ(s) ⊆ Σ. The function associated with a transition τ is represented by an assertion ρ_{τ} (V, V′), called the transition relation, which relates a state s ∈ Σ to its τ-successor s′ ∈ τ(s) by referring to both unprimed and primed versions of the system variables. An unprimed version of a system variable refers to its value in s, while a primed version of the same variable refers to its value in s′. For example, the assertion x′ = x + 1 states that the value of x in s′ is greater by 1 than its value in s. For every τ ∈ T , it is required that

ρ_{τ} → T′ = T,

i.e., the master clock is modified by no transition.

• Π : The time-progress condition. An assertion over V. The assertion is used to specify a global restriction over the progress of time.

Extended Transitions

Let Φ : ⟨V, Θ, T , Π⟩ be a clocked transition system. We define the set of extended transitions T_{T} associated with Φ as follows:

T_{T} = T ∪ {tick}.

Transition tick is a special transition intended to represent the passage of time. Its transition relation is given by:

ρ_{tick}: ∃Δ. Ω(Δ) ∧ D′ = D ∧ C′ = C + Δ,

where Ω(Δ) is given by

Ω(Δ): Δ > 0 ∧ ∀t ∈ [0, Δ). Π(D, C + t).

Let D = {u_{1}, …, u_{m}} be the set of discrete variables of Φ and C = {c_{1}, …, c_{k}} be the set of its clocks. Then, the expression C′ = C + Δ is an abbreviation for

c′_{1} = c_{1} + Δ ∧ ⋯ ∧ c′_{k} = c + Δ,

and Π(D, C + t) is an abbreviation for Π(u_{1}, …, u_{m}, c_{1} + t, …, c_{k} + t).

Runs and Computations

Let Φ : ⟨V, Θ, T , Π⟩ be a clocked transition system. A run of Φ is a finite or infinite sequence of states σ : s_{0}, s_{1}, … satisfying:

• Initiation: s_{0} ⊧ Θ

• Consecution: For each j ∈ [0, |σ|) s_{j+1} ∈ τ(s_{j}), for some τ ∈ T_{T}.

A state is called (Φ-)accessible if it appears in a run of Φ.

A computation of Φ is an infinite run satisfying:

• Time Divergence: The sequence s_{0}[T], s_{1}[T], … grows beyond any bound. That is, as i increases, the value of T at s_{i} increases beyond any bound.

A Frequently Occurring Case In many cases, the time-progress condition Π has the following special form

Π: ⋀_{i∈I}(p_{i} → t^{i} < E_{i}),

where I is some finite index set and, for each i ∈ I, the assertion p_{i} and the realvalued expression E_{i} do not depend on the clocks, and t^{i} ∈ C is some clock. This is, for example, the form of the time-progress condition for any cts representing a real-time program. For such cases, the formula Ω(Δ) can be significantly simplified and assumes the following form:

Ω(Δ): Δ > 0 ∧ ⋀_{i∈I}(p_{i} → t^{i} + Δ ≤ E_{i})

Note, in particular, that this simpler form does not use quantifications over t.

Non-Zeno Systems A cts is defined to be non-zeno if every finite run can be extended into a computation (see [AL94], [Hen92]). An equivalent formulation is that Φ is nonzeno if it satisfies

A finite sequence σ is a run of Φ iff σ is a prefix of some computation of Φ.

A consequence of Φ being non-zeno is that a state s is Φ-accessible iff it appears in some computation of Φ.

Example 1. Consider the cts’s Φ_{1} and Φ_{2} presented in Fig 1. In Fig 2, we present these two cts’s in textual form. The predicate pres(y, t, T) is an abbreviation for the assertion

pres(y, t, T): y′ = y ∧ t′ = t ∧ T′,

stating that y, t, and T, are preserved by the transition.

It is not difficult to establish that both Φ_{1} and Φ_{2} are non-zeno cts’s. This is becaues, from any accessible state, we can always move to state ℓ_{1} from which we can continue to take infinitely many time steps with increment 1.

The tick transitions for these two cts’s are given by

ρ_{tick}^{1}: ∃Δ > 0. pres(π, y) ∧ (t′, T′) = (t + Δ, T + Δ) ∧ (π = 0 → t + Δ ≤ 2)
ρ_{tick}^{2}: ∃Δ > 0. pres(π, y) ∧ (t′, T′) = (t + Δ, T + Δ) ∧ (π = 0 → t + Δ ≤ \frac{1}{2^{y+1}} ).

Following is a computation of cts Φ_{1}:

⟨π: 0 , y: 0 , t: 0 , T: 0⟩ ⟶^{tick(1)} ⟨π: 0 , y: 0 , t: 1 , T: 1⟩ ⟶^{τ_{0}}
⟨π: 0 , y: 1 , t: 1 , T: 1⟩ ⟶^{τ_{0}} ⟨π: 0 , y: 2 , t: 1 , T: 1⟩ ⟶^{tick(1)}
⟨π: 0 , y: 2 , t: 2 , T: 2⟩ ⟶^{τ_{0}} ⟨π: 0 , y: 3 , t: 2 , T: 2⟩ ⟶^{τ_{0}}
⟨π: 0 , y: 4 , t: 2 , T: 2⟩ ⟶^{τ_{1}} ⟨π: 1 , y: 4 , t: 2 , T: 2⟩ ⟶^{tick(1)}
⟨π: 1 , y: 4 , t: 3 , T: 3⟩ ⟶^{tick(1)} ⟨π: 1 , y: 4 , t: 4 , T: 4⟩ ⟶^{tick(1)}
⋯

ℓ_{0}: t < 2

y := y + 1

cts Φ_{1}

y: integer where y = 0
t, T: real where t = T = 0

ℓ_{1}:

y: integer where y = 0
t, T: real where t = T = 0

ℓ_{1}:

(y, t) := (y + 1, 0)

ℓ_{0}: t < \frac{1}{2^{y+1}}

cts Φ_{2}

Fig. 1. Two cts’s.

Note that to be a computation, time must grow beyond any bounds. Since, at location ℓ_{0} of cts time cannot grow beyond 2, any computation of Φ_{1} must eventually move to location ℓ_{1}, where time can grow beyond any bounds.

3 Programs as Clocked Transition Systems

In this section we show how to represent real-time programs as clocked transition systems.

In [MP91b], we introduced a simple programming language spl. Here we consider a subset of the language, restricting our attention to the following statements:

skip, assignment, await, noncritical, critical, conditional, concatenation, selection, while, and block.

Not including the cooperation statement has the effect that parallelism is allowed only at the top level of the program. That is, a program is a parallel copmposition of processes, each of which is sequential.

We refer the reader to Chapter 0 of [MP95] for the construction of a fair transition system F_{P} corresponding to an spl program P. This construction associates a single transition with each executable statement, which include all statements except concatenation, selection, and block. Here, we deviate from the

V: \underbrace{\{π: \{0, 1\}; y: integer\}}_{D} ∪ \underbrace{\{t, T: real\}}_{C}
Θ: π = y = t = T = 0
T : {τ_{0}, τ_{1}}with transition relations
τ_{0}: π = π′ = 0 ∧ y′ = y + 1
∧ pres(t, T)
τ_{1}: π = 0 ∧ π′ = 1 ∧ pres(y, t, T)
Π: π = 0 → t < 2
cts Φ_{1}

V: \underbrace{\{π: \{0, 1\}; y: integer\}}_{D} ∪ \underbrace{\{t, T: real\}}_{C}
Θ: π = y = t = T = 0
T : {τ_{0}, τ_{1}}with transition relations
τ_{0}: π = π′ = t′ = 0 ∧ y′ = y + 1
∧ pres(T)
τ_{1}: π = 0 ∧ π′ = 1 ∧ pres(y, t, T)
Π: π = 0 → t < \frac{1}{2^{y+1}}
cts Φ_{2}

Fig. 2. The two cts’s in textual form.

construction of [MP95] in the transition associated with the await statement. Instead, we associate with each statement of the form

ℓ: await c; ℓ̂:

a transition τ_{ℓ}, whose transition relation ρ_{ℓ} is given by

ρ_{ℓ}: ℓ ∈ π ∧ ( \begin{matrix}c ∧ π′ = π − \{ℓ\} ∪ \{ℓ̂\} \\ ∨ \\ ¬c ∧ π′ = π \end{matrix} ) ∧ pres(V − \{π\}).

Otherwise than the await statement, we follow [MP95] in the association of transitions with executable statements.

Another difference from [MP95] is that we only associate transitions with the executable statements and do not add the idling transition τ_{I}.

Let P be an spl program. To obtain a real-time program, we associate with each S, an executable statement of P, a pair of values [l_{S}, u_{S}], called the lower and upper bounds of S. These values, satisfying 0 ≤ l_{S} ≤ u_{S} ≤ ∞, are intended to provide a lower and upper bound on the length of time the statement can be enabled without being taken. We refer to a program with an assignment of time bounds as an spl_{T} program, and view it as a real-time program.

Note that assigning time bounds to each executable statement of P is equivalent to assigning time bounds [l_{τ} , u_{τ}] to each transition τ associated with an executable statement.

3.1 The cts corresponding to an spl_{T} program

Let P be an spl_{T} program. That is, an spl program with time bounds [l_{τ} , u_{τ}] associated with each transition τ ∈ T_{P} − {τ_{I} }. We will show how to construct a cts Φ_{P} corresponding to the spl_{T} program P.

As a first step, we construct the fts F_{P}: ⟨V, Θ, T , J , C⟩ corresponding to program P. Note that if program P uses only the statements in the previously presented subset, then J = T − {τ_{I} } and C = ∅. Assume that program P is a parallel composition of m processes. That is, P has the form

declarations; P_{1} ∥ ⋯ ∥ P_{m},

where each P_{i} is a (sequential) statement.

The cts corresponsing to P is given by Φ_{P}: ⟨Ṽ, Θ̃, T̃, Π⟩, where

• System Variables: Ṽ = V ∪ {t_{1}, …, t_{m}, T }.

Thus, Ṽ consists of the system variables of F_{P}, to which we add m+1 clocks, one clock t_{i} for each process P_{i}, i = 1, …, m, plus the master clock T.

• Initial Condition: Θ̃: Θ ∧ t_{1} = ⋯ = t_{m} = T = 0.

• Transitions: T̃: {τ̃ | τ ∈ T − {τ_{I} }}.

Let τ ∈ T − {τ_{I} } be a transition corresponding to an executable statement in process P_{i}. The transition relation for transition τ̃ is given by:

ρ̃_{τ}: ρ_{τ} ∧ t_{i} ≥ l_{τ} ∧ t′_{i} = 0 ∧ pres(t_{1}, …, t_{i−1}, t_{i+1}, …, t_{m}, T).

Thus, the transition can be taken only when t_{i}, the clock correponding to process P_{i}, is not below l_{τ}, the lower bound associated with τ. When taken, the transition resets clock t_{i} to 0.

• Time-progress condition Π: For each executable statement

ℓ: S

in process P_{i}, Π includes the conjunct

ℓ ∈ π → t_{i} < u_{S},

where u_{S} is the upper bound associated with statement S. This ensures that control cannot wait at location ℓ for more than u_{S} without the transition associated with S (or another transition causing control to move away from ℓ) being taken.

Note that the lower bounds of statements are added as constraints to transitions, while the upper bounds are added as constraints to the time-progress condition Π.

Example 2. Figure 3 presents a simple program consisting of two processes communicating by the shared variable x.

To make it an spl_{T} program, we uniformly associate each of its executable statements with the time bounds [3, 5]. The cts Φ_{_{ANY-Y}_{[3,5]}} associated with any-y_{[3,5]} is defined as follows:

• System Variables: V = {π, x, y, t_{1}, t_{2}, T }. In addition to the control variable π and data variables x and y, the system variables also include clock t_{1}, measuring delays in process P_{1}, clock t_{2}, measuring delays in process P_{2}, and the master clock T, measuring time from the beginning of the computation.

• Initial Condition:

Θ : π = {ℓ_{0}, m_{0}} ∧ x = y = 0 ∧ t_{1} = t_{2} = T = 0.

x, y: integer where x = y = 0

\begin{matrix}[ \begin{matrix}ℓ_{0} : & while x = 0 do \\ ℓ_{1} : y := y + 1 \\ ℓ_{2} : \end{matrix} ] & \left[{m_{0} : x := 1 \atop m_{1} :}\right] \\ − P_{1} − & − P_{2} − \end{matrix}

Fig. 3. Program any-y.

• Transitions: T : {ℓ_{0}, ℓ_{1}, m_{0}} with transition relations:

ρ_{ℓ_{0}} : ℓ_{0} ∈ π ∧ ( \begin{matrix}x = 0 ∧ π′ = π − \{ℓ_{0}\} ∪ \{ℓ_{1}\} \\ ∨ \\ x ≠ 0 ∧ π′ = π − \{ℓ_{0}\} ∪ \{ℓ_{2}\} \end{matrix} ) ∧ t_{1} ≥ 3 ∧ t′_{1} = 0
∧ pres(V − {π, t_{1}})
ρ_{ℓ_{1}} : ℓ_{1} ∈ π ∧ π′ = π − {ℓ_{1}} ∪ {ℓ_{0}} ∧ y′ = y + 1 ∧ t_{1} ≥ 3 ∧ t′_{1} = 0
∧ pres(V − {π, y, t_{1}})
ρ_{m_{0}} : m_{0} ∈ π ∧ π′ = π − {m_{0}} ∪ {m_{1}} ∧ x′ = 1 ∧ t_{2} ≥ 3 ∧ t′_{2} = 0
∧ pres(V − {π, x, t_{2}}).

• Time-progress condition:

Π : (at_{−}ℓ_{0,1} → t_{1} < 5) ∧ (at_{−}m_{0} → t_{2} < 5)

The tick transition for this system is given by

tick: ∃Δ > 0. pres(π, x, y) ∧ (t′_{1}, t′_{2}, T′) = (t_{1} + Δ, t_{2} + Δ, T + Δ) ∧
(at_{−}ℓ_{0,1} → t_{1} + Δ ≤ 5) ∧ (at_{−}m_{0} → t_{2} + Δ ≤ 5)

3.2 Specification Language

To specify properties of reactive systems, we use the language of temporal logic, as presented in [MP91b]. We use only the following:

• State formulas (assertions) - any first-order formula. For locations ℓ_{i}, ℓ_{j},

and ℓ_{k}, we denote:

at_{−}ℓ_{i} : ℓ_{i} ∈ π
at_{−}ℓ_{j,k} : at_{−}ℓ_{j} ∨ at_{−}ℓ_{k}

• � p — Always p, where p is an assertion. We refer to such a formula as an invariance formula.

• p ⇒ (q W r) — p entails q waiting for r, where p, q, and r are assertions. We refer to such a formula as a waiting-for formula.

• p ⇒ � r — p entails eventually r, where p and r are assertions. We refer to such a formula as a response formula.

For a state s and assertion p, we write s ⊧ p to indicate that p holds (is true) over s. Let σ : s_{0}, s_{1} … be an infinite sequence of states, to which we refer as a model. For an assertion p, we say that j ≥ 0, is a p-position if s_{j} ⊧ p. Satisfaction of (the three considered) temporal formulas over a model σ is defined as follows:

• A model σ satisfies the invariance formula � p, written σ ⊧ � p, if all positions within σ are p-positions.

• A model σ satisfies the waiting-for formula p ⇒ (q W r)r, written σ ⊧ p ⇒ (q W r), if every p-position i within σ initiates an interval of positions, all of which satisfy q. This continuous-q interval can either extend to infinity or terminate in an r-position which is not in the interval. That is,

σ[i] ⊧ p implies σ[j] ⊧ q for all j ≥ i, or

σ[k] ⊧ r for some k ≥ i and σ[j] ⊧ q for all j, i ≤ j < k.

• A model σ satisfies the response formula p ⇒ � r, written σ ⊧ p ⇒ � r, if every p-position i within σ is followed by an r-position j ≥ i.

A temporal formula φ is said to be valid over cts Φ (or Φ-valid) if σ ⊧ φ for every computation σ of Φ. We write Φ ⊧ φ to indicate this fact. An assertion p is called Φ-state valid if it holds at every Φ-accessible state. We write Φ ⊧ p to indicate that assertion p is Φ-state valid.

In the case that cts Φ is derived from an spl_{T} program P, we use the terms P -valid, P -state valid, and P -accessible as synonymous to Φ_{P} -valid, Φ_{P} -state valid, and Φ_{P} -accessible. We also write P ⊧ φ and P ⊧ p to denote Φ_{P} ⊧ φ and Φ_{P} ⊧ p, respectively.

4 Verifying Safety Properties of Clocked Transition Systems

In this section, we present methods for verifying safety properties of clocked transitions systems.

4.1 The Invariance Rule

A temporal formula φ that is valid over a program P specifies a property of P, i.e., states a condition that is satisfied by all computations of P. As is explained in [MP91b], the properties expressible by temporal logic can be arranged in a hierarchy that identifies different classes of properties according to the form of formulas expressing them.

Here we will consider only invariance properties, namely, properties that can be expressed by the formula � p, for some assertion p.

For assertions φ and p,

A1. φ → p
A2. Θ → φ

A3. ρ_{τ} ∧ φ → φ′ for every τ ∈ T_{T}

Φ ⊧ p

Fig. 4. Rule acc (Φ-state validity of assertion p).

The Accessibility Rule

As a preliminary step, we introduce a rule that establishes the Φ-validity of an assertion p. This is rule acc, presented in Fig. 4.

The rule uses an auxiliary assertion φ. Premise A1 of rule acc requires that the auxiliary assertion φ implies assertion p, whose Φ-state validity we wish to prove. Premise A2 of the rule requires that Θ, the initial condition of P, implies the auxiliary assertion φ. Premise A3 requires that all transitions in T_{T}^{Φ} (extended transitions of Φ) preserve φ. Premises A2 and A3 state that φ holds at the initial state of every run and that it propagates from any state to its τ-successor, for every transition τT_{T} of the system. Thus, every state in each run of Φ satisfies φ. Due to the implication A1, every such state also satisfies p. It follows that p holds on every accessible state of system Φ and, therefore, assertion p is Φ-state valid.

Rule inv

Assume that we have shown that assertion p is Φ-state valid, i.e., every accessible state of Φ satisfies p. Since all states appearing in a computation are accessible (every computation is a run), all states in every computation satisfy p. It follows that every computation of Φ satisfies � p. Thus, we may use the premises of rule acc to establish that the temporal formula � p is Φ-valid. Consequently, we propose rule inv, presented in Fig. 5, as the main tool for verifying invariance properties of a cts Φ.

Example 3. We use rule inv to establish the invariance of the assertion

p: at_{−}ℓ_{0,1} ∨ at_{−}m_{1}

over program any-y (Fig. 3). This assertion claims that, at every state in the execution of program any-y, either control of process P_{1} is at ℓ_{0} or ℓ_{1}, or control of P_{2} is at m_{1}. In particular, it implies that if P_{1} is at ℓ_{2} then P_{2} has already arrived in m_{1}.

We apply rule inv to this choice of p, taking

φ: (x = 0 ∧ at_{−}ℓ_{0,1}) ∨ at_{−}m_{1}

For assertions φ and p,

I1. φ → p

I2. Θ → φ

I3. ρ_{τ} ∧ φ → φ′ for every τ ∈ T_{T}

Φ ⊧ � p

Fig. 5. Rule inv (invariance) applied to cts Φ.

as the auxiliary assertion.

Premise I1 assumes the form

\underbrace{(x = 0 ∧ at_{−}ℓ_{0,1}) ∨ at_{−}m_{1}}_{φ} → \underbrace{at_{−}ℓ_{0,1} ∨ at_{−}m_{1}}_{p},

which is obviously valid.

Premise I2 assumes the form

\underbrace{π = \{ℓ_{0}, m_{0}\} ∧ x = 0 ∧ ⋯}_{Θ} → \underbrace{(x = 0 ∧ at_{−}ℓ_{0,1}) ∨ ⋯}_{φ}

which is obviously valid.

Premise I3 has to be checked for each τ ∈ {ℓ_{0}, ℓ_{1}, m_{0}, tick}. For example, premise I3 for ℓ_{0} assumes the form

\begin{matrix}( \underbrace{⋯ ∧ ( \begin{matrix}x = 0 ∧ π′ = π − \{ℓ_{0}\} ∪ \{ℓ_{1}\} \\ ∨ \\ x ≠ 0 ∧ π′ = π − \{ℓ_{0}\} ∪ \{ℓ_{2}\} \end{matrix} ) ∧ x′ = x ∧ ⋯}_{ρ_{ℓ_{0}}} ; ∧ \underbrace{(x = 0 ∧ (ℓ_{0} ∈ π ∨ ℓ_{1} ∈ π)) ∨ m_{1} ∈ π}_{φ} ) → \\ \underbrace{(x′ = 0 ∧ (ℓ_{0} ∈ π′ ∨ ℓ_{1} ∈ π′)) ∨ m_{1} ∈ π′}_{φ′} . \end{matrix}

It is not difficult to see that this implication is valid.

This establishes the P -validity of the invariant � p, i.e.,

P ⊧ � (at_{−}ℓ_{0,1} ∨ at_{−}m_{1}).

For assertions p and q and transition τ, we introduce the abbreviation

{p}τ{q}  standing for  ρ_{τ} ∧ p → q′.

Invariance Verification Diagrams

An effective way of presenting the verification of an invariance property by rule inv is provided by the graphical formalism of verification diagrams [MP94]. An (invariance) verification diagram is a directed labeled graph, constructed as follows:

• Nodes in the graph are labeled by assertions φ_{1}, …, φ_{m}. We will often refer to a node by the assertion labeling it.

• Edges in the graph represent transitions between assertions. Each edge departs from one node, connects to another, and is labeled by the name of a transition in the program. We refer to an edge labeled by τ as a τ-edge.

• Some of the nodes are designated as initial nodes. They are annotated by an entry arrow .

For example, in Fig. 6 we present a verification diagram for program any-y.

φ_{1} : x = 0 ∧ at_{−}ℓ_{0,1} m_{0}  φ_{2} : at_{−}m_{1}

Fig. 6. Verification Diagram D_{1}

Verification Conditions for Diagrams

With each verification diagram, we associate the following verification conditions:

• Let φ_{1} be the (single) initial node in the diagram. The verification condition corresponding to premise I2 of rule inv is given by

Θ → φ_{1}.

• Let φ be a node in the graph, τ be a transition in the program, and let φ_{1}, …, φ_{k} be the nodes reached by τ-edges departing from φ. The case that no τ-edges depart from φ, i.e., k = 0, is also included. The verification condition associated with φ and τ (corresponding to premise I3) is given by

{φ} τ {φ ∨ φ_{1} ∨ … ∨ φ_{k}}

For example, the verification conditions associated with diagram D_{1} (Fig. 6), are:

I2:  Θ → x = 0 ∧ at_{−}ℓ_{0,1}
I3 for φ_{1} and ℓ_{0} :  {x = 0 ∧ at_{−}ℓ_{0,1}} ℓ_{0} {x = 0 ∧ at_{−}ℓ_{0,1}}
I3 for φ_{1} and ℓ_{1} :  {x = 0 ∧ at_{−}ℓ_{0,1}} ℓ_{1} {x = 0 ∧ at_{−}ℓ_{0,1}}
I3 for φ_{1} and m_{0} : {x = 0 ∧ at_{−}ℓ_{0,1}} m_{0} {(x = 0 ∧ at_{−}ℓ_{0,1}) ∨ at_{−}m_{1}}
I3 for φ_{1} and tick : {x = 0 ∧ at_{−}ℓ_{0,1}} tick {x = 0 ∧ at_{−}ℓ_{0,1}}
I3 for φ_{2} and ℓ_{0} :  {at_{−}m_{1}} ℓ_{0} {at_{−}m_{1}}
I3 for φ_{2} and ℓ_{1} :  {at_{−}m_{1}} ℓ_{1} {at_{−}m_{1}}
I3 for φ_{2} and m_{0} : {at_{−}m_{1}} m_{0} {at_{−}m_{1}}
I3 for φ_{2} and tick : {at_{−}m_{1}} tick {at_{−}m_{1}}

We say that a verification diagram is valid if all the verification conditions associated with the diagram are valid.

Let D_{P} be a verification diagram associated with a program P. Let φ_{1}, …, φ_{m} be the assertions labeling the nodes of D_{P}.

Claim 1 If the verification diagram D_{P} is valid, then

P ⊧ � ⋁_{i=1}^{m} φ_{i}

If, in addition, φ_{i} → p for every i = 1, …, m, then

P ⊧ � p.

For example, all the verification conditions associated with diagram D_{1} are valid and the verification diagram D_{1} establishes

any-y ⊧ (at_{−}ℓ_{0,1} ∨ at_{−}m_{1}) (1)

Encapsulation Conventions

There are several encapsulation conventions that improve the presentation and readability of verification diagrams. We extend the notion of a directed graph into a structured directed graph by allowing compound nodes that may encapsulate other nodes, and edges that may depart or arrive at compound nodes. A node that does not encapsulate other nodes is called a basic node.

We use the following conventions:

• Labels of compound nodes: A diagram containing a compound node n, labeled by an assertion φ and encapsulating nodes n_{1}, …, n_{k} with assertions φ_{1}, …, φ_{k}, is equivalent to a diagram in which n is unlabeled and nodes n_{1}, …, n_{k} are labeled by φ_{1} ∧ φ, …, and φ_{k} ∧ φ.

• Edges entering and exiting compound nodes: A diagram containing an edge e connecting node A to a compound node n encapsulating nodes n_{1}, …, n_{k} is equivalent to a diagram in which there is an edge connecting A to each n_{i}, i = 1, …, k, with the same label as e. Similarly, an edge e connecting the compound node n to node B is the same as having a separate edge connecting each n_{i}, i = 1, …, k, to B with the same label as e.

With these conventions we can draw a more detailed verification diagram establishing (1), as shown in Fig. 7.

x = 0  m_{0} ℓ_{0} ℓ_{1}  at_{−}ℓ_{0}  at_{−}m_{1} at_{−}ℓ_{1}

Fig. 7. A more detailed diagram, using encapsulation conventions

In the diagram of Fig. 7, the single assertion x = 0∧at_{−}ℓ_{0,1}, has been broken into the two sub-cases: x = 0 ∧ at_{−}ℓ_{0} and x = 0 ∧ at_{−}ℓ_{1}, explicitly displaying the fact that transitions ℓ_{0} and ℓ_{1} cause the system to move between these two sub-cases.

We also use invariance diagrams to provide succinct representations of proofs by rule inv.

Example 4. We use rule inv to prove that program any-y_{[3,5]} terminates within 15 time units, as specified by the following invariance formula:

� (T ≤ 15 ∨ (at_{−}ℓ_{2} ∧ at_{−}m_{1}))

This formula claims that every accessible state in which the program has not terminated yet (i.e., at_{−}ℓ_{2} ∧ at_{−}m_{1} does not hold), can only be observed when the master clock T has not yet passed 15. It follows that any state observed later than T = 15 must be a termination state.

The proof is presented by the invariance diagram in Fig. 8. The assertions are indexed in descending order from φ_{3} on top to φ_{0} at bottom in order to keep compatibility with the chain diagrams introduced in Section 5.

Note that no edge in the diagram is labeled by the tick transition. This implies that all verification conditions involving the tick transition are of the form {φ_{i}} tick {φ_{i}} claiming that the tick transition preserves each of the assertions appearing in the diagram.

As an example, consider the verification condition claiming that assertion

ℓ_{1} ℓ_{0} m_{0} φ_{3} : at_{−}ℓ_{0,1} ∧ at_{−}m_{0} ∧ x = 0 ∧ t_{1} ≤ 5 ∧ t_{2} = T ≤ 5 at_{−}m_{1}, x = 1 t_{1}, t_{2}, T ≥ 0  φ_{2} : at_{−}ℓ_{1} ∧ T ≤ 5 + t_{1} ≤ 10 φ_{1} : at_{−}ℓ_{0} ∧ T ≤ 10 + t_{1} ≤ 15 φ_{0} : at_{−}ℓ_{2} ∧ at_{−}m_{1}

Fig. 8. Termination of any-y within 15 time units.

φ_{1}: at_{−}ℓ_{1} ∧ T ≤ 5 + t_{1} ≤ 10 is preserved by the tick transition.

\underbrace{at_{−}ℓ_{1} ∧ T ≤ 5 + t_{1} ≤ 10}_{φ_{1}} ∧

\underbrace{Δ > 0 ∧ π′ = π ∧ T′ = T + Δ ∧ t′_{1} = t_{1} + Δ ∧ (at_{−}ℓ_{1} → t_{1} + Δ ≤ 5) ∧ ⋯}_{ρtick}

→ \underbrace{at′_{−}ℓ_{1} ∧ T′ ≤ 5 + t′_{1} ≤ 10}_{φ′_{1}}

It is not difficult to see that this implication is state-valid. Example 5. As a second example, we present a mutual-exclusion algorithm, due to M. Fischer, which functions properly only due to the timing constraints associated with the statements. Similar proofs to the one we will present here are given in [SBM92], [AL94], and [MMP92].

The algorithm is presented in Fig. 9 under the name of program mutex. By assigning all statements in mutex the uniform time bounds [L, U], we obtain the timed program mutex_{[L,U]}. Assuming that 2L > U, we prove that the mutual exclusion property

� ¬(at_{−}ℓ_{8} ∧ at_{−}m_{8})

is valid for mutex_{[L,U]}.

x: integer where x = 0

[ \begin{matrix}ℓ_{0} : loop forever do \\ [ & ℓ_{1} : noncritical ℓ_{2} : skip ℓ_{3} : while x ≠ 1 do [ \begin{matrix}ℓ_{4} : & await x = 0 \\ ℓ_{5} : & x := 1 \\ ℓ_{6} : & skip \\ ℓ_{7} : & if x = 1 then \\ & ℓ_{8} : critical \end{matrix} ] ℓ_{9} : skip ℓ_{10} : x := 0 & ] \end{matrix} ]  [ \begin{matrix}m_{0} : loop forever do \\ [ & m_{1} : noncritical m_{2} : skip m_{3} : while x ≠ 2 do [ \begin{matrix}m_{4} : & await x = 0 \\ m_{5} : & x := 2 \\ m_{6} : & skip \\ m_{7} : & if x = 2 then \\ & m_{8} : critical \end{matrix} ] m_{9} : skip m_{10} : x := 0 & ] \end{matrix} ]

− P_{1} −  − P_{2} −

Fig. 9. Program mutex, implementing Fischer’s protocol.

Let us explain informally why mutual exclusion for program mutex is guaranteed and the role of the skip statements at ℓ_{6} and m_{6}. Assume a violation of mutual exclusion in which process P_{1} ewntered its critical section (location ℓ_{8}) first and, while P_{1} is still there, process P_{2} enters m_{8}. When P_{1} entered ℓ_{8}, x was 1. For P_{2} to enter m_{8} later, it was necessary for it to set x to 2 first, which can only be done at m_{5}. Since after P_{1} set x to 1 at ℓ_{5}, P_{2} cannot pass the test for x = 0 at m_{4}, the only possibility is that P_{2} kept waiting at m_{5} while P_{1} executed ℓ_{6} and the test at ℓ_{7}. This must have taken P_{1} at least 2L, since L is the lower bound for execution of a statement. However, P_{2} cannot wait at m_{5} for as long as 2L because 2L > U and no process can delay the execution of a statement for more than U. It follows that the described scenario in which P_{2} keep waiting at m_{5} until P_{1} enters ℓ_{8} is impossible. The role of the skip statement at ℓ_{6} is therefore to introduce an additional delay of at least L time units.

The skip statements at ℓ_{9} and m_{9} are necessary to guarantee the response properties of this algorithm, and we will discuss them in the next section. The skip statements at ℓ_{2} and m_{2} represent exits out of the noncritical sections (at ℓ_{1} and m_{1}, respectively) and intention to enter the critical sections.

The property of mutual exclusion for program mutex can be stated by the invariance formula

� ¬(at_{−}ℓ_{8} ∧ at_{−}m_{8}).

A formal proof of this invariant is presented by the invariance diagram of Fig. 10.

x = 0, at_{−}ℓ_{0..7,9,10}, at_{−}m_{0..7,9,10} at_{−}ℓ_{6..10}, at_{−}m_{0..4,6,7,9,10} at_{−}ℓ_{6}, t_{2} ≥ t_{1} at_{−}ℓ_{7}, t_{2} ≥ t_{1} + L at_{−}m_{5} x = 1  x = 2 at_{−}ℓ_{0..4,6,7,9,10}, at_{−}m_{6..10} at_{−}ℓ_{5} at_{−}m_{6}, t_{2} ≥ t_{1} at_{−}m_{7}, t_{2} ≥ t_{1} + L ℓ_{10} ℓ_{5}  ℓ_{6}  m_{5} m_{10}  m_{5} m_{5} ℓ_{5} t_{1}, t_{2} ≥ 0

Fig. 10. Mutual exclusion for program mutex.

Note that the edge labeled ℓ_{5} reaches the compound node labeled x = 1. By the encapsulation conventions, this is equivalent to having this edge connect to the basic node labeled at_{−}ℓ_{6..10}, at_{−}m_{0..4,6,7,9,10} and the compound node labeled at_{−}m_{5}. While reaching this compound node, it should enter some of its contained basic nodes. The default-entry arrow marks the basic node labeled at_{−}ℓ_{6}, t_{2} ≥ t_{1} as the single node entered by the ℓ_{5} edge. Thus, the ℓ_{5} edge connects to the basic node labeled at_{−}ℓ_{6..10}, at_{−}m_{0..4,6,7,9,10} and the one labeled at_{−}ℓ_{6}, t_{2} ≥ t_{1}.

Completeness of Rule inv

Rule inv is complete for verifying invariances of fair transition systems. This is stated by the following claim.

Claim 2 If formula � p is valid over non-zeno cts P, then there exists an assertion φ such that premises I1-I3 of rule inv are state-valid.

Justification The basic idea of the proof is the construction of an assertion acc_{P} that holds in a state s iff s is P -accessible, i.e., appears in some run of P. We then show that if � p is P -valid, then the premises of rule inv are state-valid (implying that they are also P -state valid) when taking acc_{P} for φ. Since we are only proving relative completeness, it is enough to show validity of the premises, assuming an oracle that provides proofs or otherwise verifies all generally valid assertions.

For the construction of acc_{P}, we refer the reader to [MP91a] or Chapter 2 of [MP95]. Assume that we have constructed an assertion acc_{P} such that

s ⊧ acc_{P}  iff  s is a P -accessible state.

We show that acc_{P}, when substituted for φ, validates the three premises of rule inv.

I1. acc_{P} → p By our assumption that � p is P -valid, it follows that each state appearing in some computation satisfies p. As P is non-zeno, every accessible state appears in some computation and, hence, every accessible state satisfies p. Since acc_{P} characterizes precisely the accessible states, the premise follows.

I2. Θ → acc_{P} It is obvious that every state satisfying Θ is initial and is, therefore, P - accessible. Consequently, such a state must satisfy acc_{P}, which characterizes all P -accessible states.

I3. ρ_{τ} (U, Ũ) ∧ acc_{P} (U) → acc_{P} (Ũ), for each τ ∈ T and every values of U and Ũ. Let U and Ũ be two lists of values, which can be viewed as values of the system variables V, such that both ρ_{τ} (U, Ũ) and acc_{P} (U) are true. We will show that acc_{P} (Ũ) is also true. Let s and s̃ be two arbitrary states such that s[V] = U and s̃[V] = Ũ. Since acc_{P} (U) = t, we have that s ⊧ acc_{P}. By the meaning of acc_{P}, it follows that s is P -accessible. From ρ_{τ} (U, Ũ) = t, it follows that ⟨s, s̃⟩ ⊧ ρ_{τ} (V, V′) and, therefore, that s̃ is a τ-successor of s. Since s is accessible, it follows that also s̃ is accessible and, hence s̃ ⊧ acc_{P}, leading to acc_{P} (Ũ) = t This concludes the proof of completeness of rule inv.

The following example demonstrates that the assumption that P is non-zeno is essential to the completeness of the rule.

Example 6. Consider the cts Φ_{3} which is presented graphically in Fig. 11 and textually in Fig. 12.

ℓ_{0}  t := 0  ℓ_{1}: t < 1^{Fig. 11. cts Φ_{3}.}

Clearly, cts Φ_{3} is a possibly-zeno system because, once a run enters location ℓ_{1}, time is bounded and cannot diverge. Thus, a run entering location ℓ_{1} cannot be extended into a computation of Φ_{3}. A result of the fact that no computation of Φ_{3} ever enters location ℓ_{1} is that the invariance formula � at_{−}ℓ_{0} is Φ_{3}-valid. However, examination of the arguments for the soundness of rule inv shows

V: {π: {0, 1}; t, T: real}
Θ: π = t = T = 0
T : {τ_{01}} with transition relations
τ_{01}: π = 0 ∧ π′ = 1 ∧ t′ = 0 ∧ T′ = T
Π: π = 1 → t < 1

Fig. 12. cts Φ_{3} in textual form.

that any assertion p, whose invariance is proven by rule inv, must hold on all accesible states. The state ⟨π: 1⟩ is accessible for cts Φ_{3} but does not satisfy at_{−}ℓ_{0}. Therefore, the Φ_{3} validity of � at_{−}ℓ_{0} cannot be proven by rule inv.

4.2 Verifying Waiting-for Formulas

The invariance formula � q states that q holds continuously from the beginning of the computation to infinity. In comparison, the waiting-for formula

p ⇒ q W r

also states the continuous holding of q but only for an interval that is initiated by an occurrence of p and may be terminated by an occurrence of r. Such formulas are useful for expressing timing properties, where time is measured since an occurrence of an event, rather than from the beginning of a computation.

Example 7. Consider program cyclic, presented in Fig. 13. This program

x, y: integer where x = y = 0

[ \begin{matrix}ℓ_{0} : loop forever do \\ [ & \begin{matrix}ℓ_{1} : & while x = 0 do \\ ℓ_{2} : y := y + 1 \\ ℓ_{3} : & x := 1 \end{matrix} & ] \end{matrix} ]  [ \begin{matrix}m_{0} : loop forever do \\ [ & \begin{matrix}m_{1} : & x := 1 \\ m_{2} : & await x = 0 \end{matrix} & ] \end{matrix} ]

− P_{1} −  − P_{2} −

Fig. 13. Program cyclic.

can be viewed as a generalization of program any-y, in which the basic interaction between processes P_{1} and P_{2} is embedded within an endless loop.

Since program cyclic never terminates, a relevant time-related property is that from any state in which we observe P_{1} at ℓ_{1} and P_{2} at m_{1}, P_{1} will reach location ℓ_{3} within at most 15 time units.

This property can be stated by the following waiting-for formula:

at_{−}ℓ_{1} ∧ at_{−}m_{1} ∧ x = 0 ∧ T = a ⇒ (T ≤ a + 15) W at_{−}ℓ_{3}.

This formulas uses a rigid variable a to record the time at the initial observation state. It claims that from the time we observe a state satisfying at_{−}ℓ_{1} ∧ at_{−}m_{1} ∧ x = 0, time will not progress by more than 15 units before we observe P_{1} at ℓ_{3}.

To facilitate the expression of such properties, we introduce the abbreviation

T_{a}: T − a.

With this abbreviation we can write the property of “reaching ℓ_{3} within 15 time units” as

at_{−}ℓ_{1} ∧ at_{−}m_{1} ∧ x = 0 ∧ T_{a} = 0 ⇒ (T_{a} ≤ 15) W at_{−}ℓ_{3}.

The T_{a} abbreviation allows us to view T_{a} as a special timer, reset at the initial point of observation.

A Waiting-for Rule

To establish the P -validity of a waiting-for formula, we may use rule wait, presented in Fig. 14.

For assertions p, q, φ, and r,

U1. φ → q

U2. p → r ∨ φ

U3. ρ_{τ} ∧ φ → r′ ∨ φ′ for every τ ∈ T_{T}

P ⊧ p ⇒ q W r

Fig. 14. Rule wait (waiting-for) applied to cts P.

Waiting Diagrams

Proofs by rule wait can be succinctly represented by special verification diagrams to which we refer as waiting diagrams.

A waiting diagram is a directed labeled graph constructed as follows:

• Nodes in the graph are labeled by assertions φ_{0}, …, φ_{m}. We will often refer to a node by the assertion labeling it. The node labeled by φ_{0} is called the terminal node and is graphically identified by being drawn with bold-face boundaries.

• Edges in the graph represent transitions between assertions. Each edge is labeled by the name of a transition in the program. We refer to an edge labeled by τ as a τ-edge. No edges depart form the terminal node.

• Some of the nodes are designated as initial nodes. They are annotated by an entry arrow.

Verification Conditions Implied by a Chain Diagram

Consider a nonterminal node labeled by assertion φ. Let τ ∈ T_{T} be a transition and let φ_{1}, …, φ_{k}, k ≥ 0, be the successors of φ by edges labeled with τ (possibly including φ itself). With each such node and transition, we associate the following verification condition:

ρ_{τ} ∧ φ → φ′ ∨ φ′_{1} ∨ ⋯ ∨ φ′_{k}.

In particular, if k = 0 (i.e., φ has no τ-successors), the associated verification condition is

ρ_{τ} ∧ φ → φ′.

Valid Waiting Diagrams

A waiting diagram is said to be valid over cts P (P -valid for short) if all the verification conditions associated with the diagram are P -state valid.

The consequences of having a valid chain diagram are stated in the following claim:

Claim 3 If D is a P -valid waiting diagram with nodes φ_{0}, …, φ_{m}, then

P ⊧ ⋁_{j=0}^{m} φ_{j} ⇒ ( ⋁_{j=0}^{m} W φ_{0}

If, in addition, φ_{0} = r,

U1: ⋁_{j=0}^{m} φ_{j} → q,  and  U2: p → ⋁_{j=0}^{m} φ_{j},

then we can conclude:

P ⊧ p ⇒ q W r.

Justification We observe first that the verification conditions associated with a waiting diagram imply premise U3 of rule wait, when we take φ to be φ_{1} ∨ ⋯ ∨ φ_{m} and r to be φ_{0}.

If we further take p = φ_{0} ∨ ⋯ ∨ φ_{m} and q = φ_{1} ∨ ⋯ ∨ φ_{m}, we find that premises U1 and U2 hold trivially. This yields the first part of the claim.

The second part of the claim considers different p and q but explicitly requires that premises U1 and U2 are P -valid. The conclusion follows by rule wait.

Example 8. In Fig. 15, we present a waiting diagram that establishes the property

at_{−}ℓ_{1} ∧ at_{−}m_{1} ∧ x = 0 ∧ T_{a} = 0 ⇒ (T_{a} ≤ 15) W at_{−}ℓ_{3}

for program cyclic.

5 Verifying Response Properties of Clocked Transition Systems

In this section, we present methods for verifying response properties of clocked transitions systems.

5.1 The Clock-Bounded Chain Rule

The basic rule for proving response properties of clocked transition systems is the clock-bounded chain rule (rule cb-chain) presented in Fig. 16. The rule uses auxiliary assertions φ_{1}, …, φ_{m} and refers to assertion q also as φ_{0}. With each assertion φ_{i} we associate one of the clocks c_{i} ∈ C, to which we refer as the helpful clock, and an upper bound b_{i}. The intention is that while remaining in states satisfying φ_{i}, the clock c_{i} is bounded by b_{i}. Since time in a computation grows beyond any bound, this will imply that we cannot continually stay at φ_{i}-state for too long.

Premise C1 requires that every p-position satisfies one of φ_{0} = q, φ_{1}, …, φ_{m}.

m_{1} at_{−}ℓ_{2} ∧ T_{a} ≤ 5 + t_{1} ≤ 10 ℓ_{2} at_{−}ℓ_{1} ∧ T_{a} ≤ 10 + t_{1} ≤ 15 ℓ_{1} 0 ≤ t_{1}, t_{2} ≤ 5, T_{a} ≥ 0 at_{−}m_{2}, x = 1  at_{−}ℓ_{3} at_{−}ℓ_{1,2} ∧ at_{−}m_{1} ∧ x = 0 ∧ T_{a} ≤ t_{2} ≤ 5

Fig. 15. A waiting diagram, establishing the formula at_{−}ℓ_{1} ∧ at_{−}m_{1} ∧ x = 0 ∧ T_{a} = 0 ⇒ (T_{a} ≤ 15) W at_{−}ℓ_{3}

Premise C2 requires that every τ-successor (for any τ ∈ T_{T}) of a φ_{i}-state s is a φ_{j}-state for some j ≤ i. In the case that the successor state satisfies φ_{i}, it is required that the transition does not decrease the value of c_{i}.

Premise C3 requires that assertion φ_{i} implies that c_{i} is bounded by the constant b_{i}.

The following claim states the soundness of the rule:

Claim 4 Rule cb-chain is sound for proving that a response formula is Φ-valid.

Justification: Assume that the premises of the rule are Φ-valid, and let σ be a computation of Φ. We will show that σ satisfies the rule’s consequence

p ⇒ � q,

i.e., every p position in σ is followed by a q-position.

Assume that p holds at position k and no later position i ≥ k satisfies q. By C1 some φ_{j} must hold at position k. Let j_{k} denote the minimal index such that φ_{j_{k}} holds at k. Obviously j_{k} > 0 by our assumption that q never occurs beyond position k.

By C2, state s_{k+1} must satisfy φ_{j} for some j, 0 < j ≤ j_{k}. Let j_{k+1} denote the minimal such index. Continuing in this manner we obtain that every position i beyond k satisfies some φ_{j_{i}}, where j_{i} > 0 and

j_{k} ≥ j_{k+1} ≥ j_{k+2} ≥ · · · .

Since we cannot have an infinite non-increasing sequence of natural numbers

For assertions p, q, and φ_{0} = q, φ_{1}, …, φ_{m},

clocks c_{1}, …, c_{m} ∈ C, and real constants b_{1}, …, b_{m} ∈ R,

C1. p → ⋁_{j=0}^{m} φ_{j}

The following two premises hold for i = 1, …, m

C2. ρ_{τ} ∧ φ_{i} → (ϖ′ ∧ c′_{i} ≥ c_{i}) ∨ ⋁_{j<i} φ′_{j}

for every τ ∈ T_{T}

C3. φ_{i} → c_{i} ≤ b_{i}

p ⇒ � q

Fig. 16. Rule cb-chain (clock-bounded chain rule for response).

which decreases infinitely many times, there must exist a position r ≥ k such that

j_{r} = j_{r+1} = j_{r+2} = · · · .

Denote the value of this eventually-stable assertion index by u = j_{r}.

Consider the value of the clock c_{u} at states s_{i}, i ≥ r. By C2, the value of c_{u} never decreases. Also, whenever a tick transition with increment Δ is taken, c_{u} increases (as do all clocks) by Δ. It follows that the master clock T cannot increase by more than b_{u} − s_{r}[c_{u}] from its value at state s_{r}. This contradicts the fact that σ is a computation in which the master clock increases beyond all bounds.

We conclude that our assumption of the existence of a p-position not followed by any q-position is false. Consequently, if the premises of the rule hold then every p-position must be followed by a q-position, establishing the consequence of the rule.

Example 9. We illustrate the use of rule cb-chain to prove the termination of program any-y_{[3,5]}, which can be stated by the response formula

at_{−}ℓ_{0} ∧ at_{−}m_{0} ∧ x = t_{1} = t_{2} = 0 ⇒ � (at_{−}ℓ_{2} ∧ at_{−}m_{2}).

To apply rule cb-chain, we identify p as at_{−}ℓ_{0} ∧ at_{−}m_{0} ∧ x = t_{1} = t_{2} = 0 and q as at_{−}ℓ_{2} ∧ at_{−}m_{2}. The auxiliary assertions, helpful clocks, and bounds are presented in the following table:

φ_{0}: at_{−}ℓ_{2} ∧ at_{−}m_{2}  −  −
φ_{1}: at_{−}ℓ_{0} ∧ at_{−}m_{1} ∧ x = 1 ∧ t_{1} ≤ 5  c_{1}: t_{1}  b_{1}: 5
φ_{2}: at_{−}ℓ_{1} ∧ at_{−}m_{1} ∧ x = 1 ∧ t_{1} ≤ 5  c_{2}: t_{1}  b_{1}: 5
φ_{3}: at_{−}ℓ_{0,1} ∧ at_{−}m_{0} ∧ x = 0 ∧ t_{1} ≤ 5 ∧ t_{2} ≤ 5  c_{3}: t_{2}  b_{1}: 5

We check the premises of rule cb-chain for this selection of auxiliary assertions, helpful clocks, and bounds.

• Premise C1 assumes the form

\underbrace{at_{−}ℓ_{0} ∧ at_{−}m_{0} ∧ x = y = t_{1} = t_{2} = T = 0}_{p} →

\underbrace{⋯ ∨ at_{−}ℓ_{0,1} ∧ at_{−}m_{0} ∧ x = 0 ∧ t_{1} ≤ 5 ∧ t_{2} ≤ 5}_{··· ∨ φ_{3}},

which is obviously state valid.

• Premise C2 has to be checked for each i = 1, …, m and each τ ∈ T_{T}. We present only few representative cases. Premise C2 for φ_{3} and transition m_{0} assumes the form

\underbrace{π′ = π − \{m_{0}\} ∪ \{m_{1}\} ∧ x′ = 1 ∧ t′_{1} = t_{1} ∧ ⋯}_{ρ_{m_{0}}} ∧ \underbrace{at_{−}ℓ_{0,1} ∧ t_{1} ≤ 5 ∧ ⋯}_{φ_{3}}

→ ( \begin{matrix}& ⋯ \\ ∨ & \underbrace{at′_{−}ℓ_{0} ∧ at′_{−}m_{1} ∧ x′ = 1 ∧ t′_{1} ≤ 5}_{φ′_{1}} \\ ∨ & \underbrace{at′_{−}ℓ_{1} ∧ at′_{−}m_{1} ∧ x′ = 1 ∧ t′_{1} ≤ 5}_{φ′_{2}} \end{matrix} )_{,}

which is obviously state valid. Premise C2 for φ_{2} and the tick transition assume the form

\underbrace{Δ > 0 ∧ π′ = π ∧ x′ = x ∧ t′_{1} = t_{1} + Δ ∧ (at_{−}ℓ_{0,1} → t_{1} + Δ ≤ 5) ∧ ⋯}_{ρtick}

∧ \underbrace{at_{−}ℓ_{1} ∧ at_{−}m_{1} ∧ x = 1 ∧ t_{1} ≤ 5}_{φ_{2}} →

\underbrace{at′_{−}ℓ_{1} ∧ at′_{−}m_{1} ∧ x′ = 1 ∧ t′_{1} ≤ 5}_{φ′_{2}} ,

which is obviously state valid.

• Premise C3 is trivially valid, since each φ_{i}, i = 1, …, 3 includes c_{i} ≤ b_{i} as a conjunct.

This analysis indicates that all premises of rule cb-chain are state valid. It follows that the reponse formula

at_{−}ℓ_{0} ∧ at_{−}m_{0} ∧ x = t_{1} = t_{2} = 0 ⇒ � (at_{−}ℓ_{2} ∧ at_{−}m_{2})

is valid over program any-y_{[3,5]}.

5.2 Clock-Bounded Chain Diagrams

The main ingredients of a proof by rule cb-chain can be conveniently and effectively presented by a special type of verification diagrams that summarizes the auxiliary assertions with their helpful clocks and bounds, and display the possible transitions between the assertions.

We define a clock bounded chain diagram (chain diagram for short) to be a directed labeled graph constructed as follows:

• Nodes in the graph are labeled by assertions. Each node is labeled by a pair of assertions: ϕ_{i} and β_{i}, for i = 0, …, m. The assertion β_{i} has the form c_{i} ≤ b_{i}, where c_{i} ∈ C is a clock and b_{i} is a real constant. We refer to the conjunction ϕ_{i} ∧ β_{i} as φ_{i}, and say that the node is labeled by the (combined) assertion φ_{i}. We often refer to nodes by the assertion φ_{i} labeling them. The node labeled by φ_{0} is called the terminal node and is graphically identified by being drawn with bold-face boundaries.

• Edges in the graph represent transitions between assertions. Each edge connects one assertion to another and is labeled by one or more transitions. An edge can connect node φ_{i} to node φ_{j} only if i ≥ j. This imposes the restriction that the graph of a chain diagram is weakly acyclic, i.e., the only cycles in the graph consist of a node connected to itself.

Verification Conditions Implied by a Chain Diagram

Consider a nonterminal node labeled by assertion φ: ϕ ∧ β where the clock-bound assertion is β: c ≤ b. Let τ ∈ T_{T} be a transition and let φ_{1}, …, φ_{k}, k ≥ 0, be the successors of φ by edges labeled with τ (possibly including φ itself). With each such node and transition, we associate the following verification condition:

ρ_{τ} ∧ φ → (φ′ ∧ c′ ≥ c) ∨ φ′_{1} ∨ ⋯ ∨ φ′_{k}.

In particular, if k = 0 (i.e., φ has no τ-successors), the associated verification condition is

ρ_{τ} ∧ φ → φ′ ∧ c′ ≥ c.

Valid Chain Diagrams

A chain diagram is said to be valid over cts Φ (Φ-valid for short) if all the verification conditions associated with the diagram are Φ-state valid.

The consequences of having a valid chain diagram are stated in the following claim:

Claim 5 If D is a Φ-valid chain diagram with nodes φ_{0}, …, φ_{m}, then

Φ ⊧ ⋁_{j=0}^{m} φ_{j} ⇒ � φ_{0}

If, in addition, φ_{0} = q and

C1: p → ⋁_{j=0}^{m} φ_{j},

then we can conclude:

Φ ⊧ p ⇒ � q.

The claim follows from the observation that the verification conditions associated with a chain diagram precisely correspond to premise C2 of rule cb-chain. Premise C1 is trivially satisfied for the first part of the claim, where we take p to be ⋁_{j=0}^{m} φ_{j}. It is explicitly provided in the second part of the claim. Premise C3 is trivially satisfied by having β_{i}: c_{i} ≤ b_{i} as an explicit conjunct of varp_{i} = ϕ_{i} ∧ β_{i}.

Example 10. In Fig. 17, we present a chain diagram for proving that

at_{−}ℓ_{0} ∧ at_{−}m_{0} ∧ x = t_{1} = t_{2} = 0 ⇒ � (at_{−}ℓ_{2} ∧ at_{−}m_{2})

is valid over program any-y_{[3,5]}.

Note the use of encapsulation in labeling the compound node by the common clock bound B: t_{1} ≤ 5, which is factored out of nodes φ_{1} and φ_{2}. We also remove the index from the β assertion labeling a node and write β instead of β_{i}.

5.3 Winning a Race

We introduce an additional graph-structuring convention which leads to a more economic and comprehensible verification diagrams. Similar to the previously introduced encapsulation conventions, this one is also inspired by the Statechart language [Har87].

A conjunctive compound node is a compound node which contains two sets of encapsulated nodes: {ϕ_{1}, …, ϕ_{m}} and {ψ_{1}, …, ψ_{n}}. The two sets are separated by a dashed line. Edges may connect nodes within each of the sets, and external nodes to nodes in each of the sets. No edge may connect a ϕ-node to a ψ-node. We also allow a multi-source edge such as the edge connecting nodes ϕ_{2} and ψ_{2} to the external node χ.

In Fig. 18, we present a graph with a conjunctive compound node.

Any diagram containing conjunctive nodes can be expanded into an equivalent flat diagram, to which we refer as the expanded diagram, as follows:

• For each i ∈ {1, …, m} and j ∈ {ψ_{1}, …, n}, the expanded diagram contains a node, labeled by the conjunction ϕ_{i} ∧ ψ_{j}.

• For each τ-labeled edge connecting ϕ_{a} to ϕ_{b}, there are τ-labeled edges connecting expanded node ϕ_{a} ∧ ψ_{j} to ϕ_{b} ∧ ψ_{j} for all j ∈ {1, …, n}.

• For each τ-labeled edge connecting ψ_{c} to ψ_{d}, there are τ-labeled edges connecting expanded node ϕ_{i} ∧ ψ_{c} to ϕ_{i} ∧ ψ_{d} for all i ∈ {1, …, m}.

• For each τ-labeled edge connecting ϕ_{a} to external node χ, there are τ-labeled edges connecting expanded node ϕ_{a} ∧ ψ_{j} to χ for all j ∈ {1, …, n}.

t_{1}, t_{2}, T ≥ 0  m_{0} at_{−}m_{1}, x = 1, t_{1} ≤ 5, β: t_{1} ≤ 5 ϕ_{1} : at_{−}ℓ_{0} φ_{0} = ϕ_{0} : at_{−}ℓ_{2} ∧ at_{−}m_{1} ℓ_{0} ℓ_{1} \begin{matrix}ϕ_{3} : at_{−}ℓ_{0,1} ∧ at_{−}m_{0} ∧ x = 0 ∧ t_{1} ≤ 5 ∧ t_{2} ≤ 5 \\ β: t_{2} ≤ 5 \end{matrix} ϕ_{2} : at_{−}ℓ_{1}

Fig. 17. Verifying termination of program any-y_{[3,5]}.

• For each τ-labeled edge connecting ψ_{c} to external node χ, there are τ-labeled edges connecting expanded node ϕ_{i} ∧ ψ_{c} to χ for all i ∈ {1, …, m}.

• For each τ-labeled multi-source edge connecting nodes ϕ_{a} and ψ_{c} to external node χ, there exists a τ-labeled edge connecting expanded node ϕ_{a} ∧ ψ_{c} to node χ.

In Fig. 19, we present the flat diagram equivalent to the diagram of Fig. 18.

Analyzing Races between Processes Conjunctive nodes are particularly helpful for proving that one process always wins in a race against a competing process. Consider the trivial program race presented in Fig. 20.

As in the case of program mutex_{[L,U]}, we assign to all statements of program race time bounds [L, U], stipulating that 2L > U. It is clear that when this

τ_{1} τ_{2}  χ τ_{3}  τ_{4} ϕ_{1}  ϕ_{2} ψ_{1}  ψ_{2}

Fig. 18. A conjunctive compound node.

χ ϕ_{1} ∧ ψ_{1}  ϕ_{2} ∧ ψ_{1} ϕ_{1} ∧ ψ_{2}  ϕ_{2} ∧ ψ_{2} τ_{3}  τ_{3} τ_{1}  τ_{1} τ_{2}  τ_{2}  τ_{4}

Fig. 19. An expanded equivalent to the conjunctive diagram.

program is run, process P_{1} will terminate before P_{2} does. This is because P_{1} mst terminate within 2U time units, while P_{2} must take at least 4L > 2U time units to terminate. How do we formally prove this property which can be stated by the response formula

at_{−}ℓ_{0} ∧ at_{−}m_{0} ∧ t_{1} = t_{2} = T = 0 ⇒ � (at_{−}ℓ_{2} ∧ at_{−}m_{0..3}) ?

In Fig. 21, we present a chain diagram which proves this property.

[ \begin{matrix}ℓ_{0} : & skip \\ ℓ_{1} : & skip \\ ℓ_{2} : \end{matrix} ]  [ \begin{matrix}m_{0} : & skip \\ m_{1} : & skip \\ m_{2} : & skip \\ m_{3} : & skip \\ m_{4} : \end{matrix} ]

− P_{1} −  − P_{2} −

Fig. 20. Program race.

m_{0} m_{1} m_{2} at_{−}m_{0} ∧ T = t_{2} at_{−}m_{1} ∧ T ≥ t_{2} + L at_{−}m_{2} ∧ ≥ t_{2} + 2L at_{−}m_{3} ∧ ≥ t_{2} + 3L at_{−}ℓ_{2} ∧ at_{−}m_{0..3} t_{1}, t_{2}, T ≥ 0, β : t_{1} ≤ U at_{−}ℓ_{0} ∧ T = t_{1} ≤ U ℓ_{0} ℓ_{1} at_{−}ℓ_{1} ∧ T ≤ U + t_{1} ≤ 2U

Fig. 21. Chain diagram proving that P_{1} wins the race.

A central argument in the validation of this diagram is that transition m_{2} is disabled on all nodes within the conjunctive compound node. Transition m_{2} can be enabled only on an at_{−}m_{2}-state and only when t_{2} ≥ L. Combining the assertion attached to the m_{2} node with t_{2} ≥ L, we obtain T ≥ 2L > 4U. However, all assertions on the left-hand side of the conjunctive node imply T ≤ 4U. This shows that m_{2} is disabled on all states covered by the conjunctive node, and the only exit is via ℓ_{1}.

This establishes the property

at_{−}ℓ_{0} ∧ at_{−}m_{0} ∧ t_{1} = t_{2} = T = 0 ⇒ � (at_{−}ℓ_{2} ∧ at_{−}m_{0..3}).

5.4 Proving Accessibility for Program mutex_{[L,U]}

As a more ambitious example, we prove for program mutex_{[L,U]} the property of accessibility which can be stated (for process P_{1}) by the response formula

at_{−}ℓ_{2} ⇒ � at_{−}ℓ_{9}.

A similar formula states accessibility for process P_{2}.

From the invariance diagram of Fig. 10, we can infer the following four invariants, which we will use in the response proof:

χ_{0}: � (x ∈ {0, 1, 2})
χ_{1}: � (at_{−}ℓ_{0..2,4,5} → x ≠ 1)
χ_{2}: � (at_{−}m_{0..2,4,5} → x ≠ 2)
χ_{3}: at_{−}ℓ_{4} ⇒ x = 0 ∨ (at_{−}m_{6..10} ∧ x = 2)

The accessibility formula is proved in several steps, verifying separately the following response formulas:

ψ_{1}: at_{−}ℓ_{2} ⇒ � at_{−}ℓ_{4}
ψ_{2}: at_{−}ℓ_{4} ∧ x = 0 ⇒

� (at_{−}ℓ_{8} ∨ (at_{−}ℓ_{4,6,7} ∧ at_{−}m_{6} ∧ x = 2 ∧ t_{2} = 0))

ψ_{3}: at_{−}ℓ_{4,6,7} ∧ at_{−}m_{6} ∧ x = 2 ∧ t_{2} = 0 ⇒
� (at_{−}ℓ_{4} ∧ at_{−}m_{0} ∧ x = 0 ∧ t_{2} = 0)
ψ_{4}: at_{−}ℓ_{4} ∧ at_{−}m_{6..10} ∧ x = 2 ⇒
� (at_{−}ℓ_{4} ∧ at_{−}m_{0} ∧ x = 0 ∧ t_{2} = 0)
ψ_{5}: at_{−}ℓ_{4} ∧ at_{−}m_{0} ∧ x = 0 ∧ t_{2} = 0 ⇒
� (at_{−}ℓ_{6} ∧ at_{−}m_{0..4} ∧ x = 1)
ψ_{6}: at_{−}ℓ_{6} ∧ at_{−}m_{0..4} ∧ x = 1 ⇒ � at_{−}ℓ_{8}

It is not difficult to see that response formulas ψ_{1}–ψ_{6} lead to the accessibility property.

We proceed to prove each of the response formulas.

Proving ψ_{1}: at_{−}ℓ_{2} ⇒ � at_{−}ℓ_{4}

Formula ψ_{1} states that, starting at ℓ_{2}, process P_{2} is guaranteed to reach ℓ_{4}. Statement ℓ_{2} is unconditional and is guaranteed to terminate within U time units. By χ_{1}, when we enter ℓ_{3} from ℓ_{2}, x is different from 1, and will remain so as long as we stay at ℓ_{3} (ℓ_{5} is the only statement that can set x to 1). Consequently, within U time units, P_{1} will proceed to ℓ_{4}.

The formal proof of ψ_{1} is provided by the chain diagram of Fig. 22

ℓ_{2}  at_{−}ℓ_{3} x ≠ 1, β : t_{1} ≤ U at_{−}ℓ_{2}  ℓ_{4} ℓ_{3}
Fig. 22. Chain diagram for ψ_{1}: at_{−}ℓ_{2} ⇒ � at_{−}ℓ_{4}.

Proving ψ_{2}

Response formula ψ_{2} is given by

at_{−}ℓ_{4} ∧ x = 0 ⇒ � (at_{−}ℓ_{8} ∨ (at_{−}ℓ_{4,6,7} ∧ at_{−}m_{6} ∧ x = 2 ∧ t_{2} = 0)).

It states that, starting at location ℓ_{4} with x = 0, process P_{1} will either reach the critical section (at ℓ_{8}), or be overtaken by process P_{2} just entering location m_{6} (and hence t_{2} = 0), while setting x to 2. In the latter case, P_{1} will be overtaken at one of the locations ℓ_{4}, ℓ_{6}, or ℓ_{7}.

The formal proof of ψ_{2} is presented by the chain diagram of Fig. 23.

β : t_{1} ≤ U at_{−}ℓ_{4} ∧ x = 0 ℓ_{4} at_{−}ℓ_{5} m_{5}  x = 1 m_{5}  at_{−}ℓ_{7} ℓ_{7} ϕ_{0}: at_{−}ℓ_{8} ∨ (at_{−}ℓ_{4,6,7} ∧ at_{−}m_{6} ∧ x = 2 ∧ t_{2} = 0) ℓ_{6} at_{−}ℓ_{6} ℓ_{5}

Fig. 23. Chain diagram for the formula

ψ_{2}: at_{−}ℓ_{4} ∧ x = 0 ⇒ � (at_{−}ℓ_{8} ∨ (at_{−}ℓ_{4,6,7} ∧ at_{−}m_{6} ∧ x = 2 ∧ t_{2} = 0)).

The diagram follows the progress of process P_{1} from ℓ_{4} with x = 0. While P_{1} is at ℓ_{4}, P_{2} may execute statement m_{5} and set x to 2, which reaches the goal ϕ_{0}. If this does not happen, P_{1} proceeds to ℓ_{5} and then to ℓ_{6}, setting x to 1. From this point on, either P_{2} will perform m_{5}, leading again to ϕ_{0}, or P_{2} will perform ℓ_{7} moving to ℓ_{8}, which is also a goal state.

Proving ψ_{3}

Response formula ψ_{3} is given by

at_{−}ℓ_{4,6,7} ∧ at_{−}m_{6} ∧ x = 2 ∧ t_{2} = 0 ⇒ � (at_{−}ℓ_{4} ∧ at_{−}m_{0} ∧ x = 0 ∧ t_{2} = 0).

The formula states that, once P_{1} has been overtaken by P_{2}, it will return to location ℓ_{4} before P_{2} exits its critical section and returns to m_{0}, setting x back to 0. The fact that, being denied entry to ℓ_{8}, process P_{1} must eventually return to ℓ_{3} and proceed to ℓ_{4} is obvious. Less obvious is the fact that when P_{2} performs m_{10} on its exit from the critical section, P_{1} is already at ℓ4. This result from the number of statements that each process has to execute until they reach ℓ_{4} and m_{0}, respectively, and from the assumption U < 2L which guarantees that P_{1} completes the execution of a single statement before P_{2} can complete the execution of two statements.

The worst case for P_{1} is if it is overtaken at ℓ_{6}. To reach ℓ_{4} it must execute 3 statements: ℓ_{6}, ℓ_{7}, and ℓ_{3}. It will take P_{1} at most 3U to do so. To reach location m_{0} from its initial location at m_{6}, P_{2} has to execute at least 6 statements: m_{6}, m_{7}, m_{8}, m_{3}, m_{9}, and m_{10}. It will take P_{2} at least 6L to reach m_{0}. Since 3U < 6L, P_{1} will get to ℓ_{3} first.

The precise analysis of this race between P_{1} and P_{2} is presented by the chain diagram of Fig. 24

at_{−}ℓ_{6} ∧ T_{a} ≤ t_{1} ≤ U ℓ_{6} at_{−}ℓ_{7} ∧ T_{a} ≤ U + t_{1} ≤ 2U ℓ_{7} at_{−}ℓ_{3} ∧ T_{a} ≤ 2U + t_{1} ≤ 3U ℓ_{3} at_{−}ℓ_{4}  m_{6} at_{−}m_{6} ∧ T_{a} = t_{2} at_{−}m_{7} ∧ T_{a} ≥ t_{2} + L m_{7} at_{−}m_{8} ∧ ≥ t_{2} + 2L m_{8} at_{−}m_{3} ∧ ≥ t_{2} + 3L m_{3} at_{−}m_{9} ∧ ≥ t_{2} + 4L m_{9} at_{−}m_{10} ∧ ≥ t_{2} + 5L m_{10} at_{−}ℓ_{4} ∧ at_{−}m_{0} ∧ x = 0 ∧ t_{2} = 0 β : t_{2} ≤ U t_{1}, t_{2}, T_{a} ≥ 0, x = 2

Fig. 24. Chain diagram for the formula

ψ_{3} : at_{−}ℓ_{4,6,7} ∧ at_{−}m_{6} ∧ x = 2 ∧ t_{2} = 0 ∧ T_{a} = 0 ⇒ � (at_{−}ℓ_{4} ∧ at_{−}m_{0} ∧ x = 0 ∧ t_{2} = 0).

Note that m_{10} is enabled only at states in which P_{1} is at ℓ_{4}. This is becaus at all other P_{1}-locations, T_{a} ≤ 3U < 6L. For m_{1}0 to be enabled, T_{a} must be at least 6L.

Proving ψ_{4}

Response formula ψ_{4} is given by

at_{−}ℓ_{4} ∧ at_{−}m_{6..10} ∧ x = 2 ⇒ � (at_{−}ℓ_{4} ∧ at_{−}m_{0} ∧ x = 0 ∧ t_{2} = 0).

The formula states that, starting with P_{1} at ℓ_{4}, x = 2, and P_{2} somewhere within {m_{6}, …, m_{10}}, we are guaranteed to reach a state in which P_{1} is still at ℓ_{4} but P_{2} has just moved to m_{0} (hence t_{2} = x = 0). This property relies on the progress of P_{2} through {m_{6}, …, m_{10}} to m_{0} while x = 2 and P_{1} cannot change the value of x, beeing stuck at ℓ_{4}. For a formal proof of this property, we can use again the diagram of Fig. 24, where the initial nodes are within the compound node labeled by at_{−}ℓ_{4}.

Proving ψ_{5}

Response formula ψ_{5} is given by

at_{−}ℓ_{4} ∧ at_{−}m_{0} ∧ x = 0 ∧ t_{2} = 0 ⇒ � (at_{−}ℓ_{6} ∧ at_{−}m_{0..4} ∧ x = 1).

The formula considers another possible race between P_{1} and P_{2}, starting with P_{1} at ℓ_{4} and P_{2} just arriving to m_{0}. Formula ψ_{5} states that P_{1} will reach ℓ_{6} (with x = 1 before P_{2} reaches m_{5}. Note that from a state satisfying at_{−}ℓ_{6} ∧ at_{−}m_{0..4} ∧ x = 1 the entry of P_{1} to its critical section is guaranteed, since P_{2} cannot pass the test at m_{4} and interefere with P_{1}’s progress.

Formula ψ_{5} is verified by the chain diagram of Fig. 25.

A simple informal argument explains why P_{1} is sure to win this race. To move from ℓ_{4} to ℓ_{6}, P_{1} has to execute 2 statements: ℓ_{4} and ℓ_{5}, which takes at most 2U. In that time, P_{2} cannot complete the execution of the 5 statements m_{0}–m_{4} necessary to reach m_{5}, since 5L > 2U.

Proving ψ_{6}

Response formula ψ_{6} is given by

ψ_{6}: at_{−}ℓ_{6} ∧ at_{−}m_{0..4} ∧ x = 1 ⇒ � at_{−}ℓ_{8}.

This formula states that, once P_{1} reached ℓ_{6} while P_{2} is still confined within the range {m_{0}, …, m_{4}}, entry of P_{1} to ℓ_{8} is guaranteed. The proof presented in the diagram of Fig. 26 simply traces the progress of P_{1} from ℓ_{6} to ℓ_{8}, while x keeps its value of 1.

This concludes the proof of accessibility for program mutex_{[L,U]}.

at_{−}m_{3} ∧ ≥ t_{2} + 3L m_{3} t_{1}, t_{2}, T_{a} ≥ 0, x = 0  β : t_{1} ≤ U at_{−}ℓ_{4} ∧ T_{a} ≤ t_{1} ≤ U ℓ_{4} at_{−}ℓ_{5} ∧ T_{a} ≤ U + t_{1} ≤ 2U  at_{−}m_{0} ∧ T_{a} = t_{2} m_{0} at_{−}m_{1} ∧ T_{a} ≥ t_{2} + L m_{1} at_{−}m_{2} ∧ ≥ t_{2} + 2L m_{2} at_{−}m_{4} ∧ ≥ t_{2} + 4L ℓ_{5}at_{−}ℓ_{6} ∧ at_{−}m_{0..4} ∧ x = 1

Fig. 25. Chain diagram for the formula

ψ_{5}: at_{−}ℓ_{4} ∧ at_{−}m_{0} ∧ x = 0 ∧ t_{2} = 0 ∧ T_{a} = 0 ⇒ � (at_{−}ℓ_{6} ∧ at_{−}m_{0..4} ∧ x = 1).

5.5 Clock-Bounded Well-Founded Rule

Rule cb-chain is adequate for proving response properties in which a q state is achieved in a number of significant steps which is a priori bounded. For example, in verifying termination of program any-y_{[3,5]}, there were 3 helpful step leading to termination. These are represented in the chain diagram of Fig. 17 by the edges entering nodes ϕ_{2}–ϕ_{0}.

In many cases, the number of helpful steps needed to reach the goal q cannot be bounded a priori. For these cases we need a stronger rule, based on wellfounded ordering.

Well-founded Domains

We define a well-founded domain (A, ≻) to consist of a set A and a well-founded order relation ≻ on A. A binary relation ≻ is called an order if it is

• transitive: a ≻ b and b ≻ c imply a ≻ c, and

• irreflexive: a ≻ a for no a ∈ A.

at_{−}m_{0..4}, x = 1, β : t_{1} ≤ U at_{−}ℓ_{6}  ℓ_{6}  at_{−}ℓ_{7}  ℓ_{7}  ℓ_{8}

Fig. 26. Chain diagram for the formula ψ_{6}: at_{−}ℓ_{6} ∧ at_{−}m_{0..4} ∧ x = 1 ⇒ � at_{−}ℓ_{8}.

The relation ≻ is called well-founded if there does not exist an infinitely descending sequence a_{0}, a_{1}, … of elements of A such that

a_{0} ≻ a_{1} ≻ · · · .

A typical example of a well-founded domain is (ℕ, >), where ℕ are the natural numbers (including 0) and > is the greater-than relation. Clearly, > is well-founded over the natural numbers, because there cannot exist an infinitely descending sequence of natural numbers

n_{0} > n_{1} > n_{2} > ….

For ≻, an arbitrary order relation on A, we define its reflexive extension ⪰ to hold between a, a′ ∈ A if either a ≻ a′ or a = a′.

Lexicographic Tuples

Another frequently used well-founded domain is (ℕ^{k}, ≻), where ℕ^{k} is the set of k-tuples of natural numbers. The order ≻ is defined by

(n_{1}, …, n_{k}) ≻ (m_{1}, …, m_{k}) iff n_{1} = m_{1}, …, n_{i−1} = m_{i−1}, n_{i} > m_{i}
for some i, 1 ≤ i ≤ k.

For example, for k = 3

(7, 2, 1) ≻ (7, 0, 45).

It is easy to show that the domain (ℕ^{k}, ≻) is well-founded.

It is possible to make lexicographic comparisons between tuples of integers of different lengths. The convention is that the relation holding between (a_{1}, …, a_{i}) and (b_{1}, …, b_{k}) for i < k is determined by lexicographically comparing (a_{1}, …, a_{i}, 0, …, 0) to (b_{1}, …, b_{i}, b_{i+1}, …, b_{k}). That is, we pad the shorter tuple by zeros on the right until it assumes the length of the longer tuple.

According to this definition, (0, 2) ≻ 0, since (0, 2) ≻ (0, 0). In a similar way, 1 ≻ (0, 2).

5.6 Rule cb-well

In Fig. 27, we present the clock-bounded well-founded response rule (rule cbwell) for proving response properties of fair transition systems. The rule uses auxiliary assertions φ_{1}, …, φ_{m} and refers to assertion q also as φ_{0}. With each assertion φ_{i}, i > 0, we associate one of the clocks c_{i} ∈ C, to which we refer as the helpful clock, and an upper bound B_{i}, which is a real-valued expression. Also required are a well-founded domain (A, ≻), and ranking functions δ_{i}: Σ ↦ A, i = 1, …, m, mapping states of the system to elements of A. The ranking functions measure progress of the computation towards the goal q.

For assertions p, q, and φ_{0} = q, φ_{1}, …, φ_{m},

clocks c_{1}, …, c_{m} ∈ C,

real expressions B_{1}, …, B_{m} ∈ R, a well-founded domain (A, ≻), and ranking functions δ_{1}, …, δ_{m}: Σ ↦ A,

W1. p → ⋁_{j=0}^{m} φ_{j}

The following two premises hold for i = 1, …, m

W2. \begin{matrix}ρ_{τ} ∧ φ_{i} → ⋁_{j=0}^{m}(φ′_{j} ∧ δ_{i} ≻ δ′_{j}) ∨ \\ (φ′_{i} ∧ δ′_{i} = δ_{i} ∧ c_{i} ≤ c′_{i} ∧ B′_{i} ≤ B_{i}) \end{matrix}

for every τ ∈ T_{T}

W3. φ_{i} → c_{i} ≤ B_{i}

p ⇒ � q

Fig. 27. Rule cb-well (clock-bounded well-founded rule for response).

Premise W1 requires that every p-position satisfies one of φ_{0} = q, φ_{1}, …, φ_{m}. Premise W2 requires that every τ-successor (for any τ ∈ T_{T}) of a φ_{i}-state s

is a φ_{j}-state for some j ≤ i, with a rank δ′_{j} not exceeding δ_{i}. In the case that the successor state satisfies φ_{i}, it is allowed that δ′_{i} = δ_{i} but is required that the transition does not decrease the value of c_{i} or increase the value of B_{i}. In all other cases it is required that δ′_{j} ≺ δ_{i}, i.e., that the rank strictly decreases.

Premise W3 requires that assertion φ_{i} implies that c_{i} is bounded by the constant B_{i}.

The following claim states the soundness of the rule:

Claim 6 Rule cb-well is sound for proving that a response formula is Φ-valid.

Justification: Assume that the premises of the rule are Φ-valid, and let σ be a computation of Φ. We will show that σ satisfies the rule’s consequence

p ⇒ � q.

Assume that Φ holds at position k and no later position i ≥ k satisfies q. By W1 some φ_{j} must hold at position k. Let u_{k} ∈ A be the minimal rank of state s_{k}, i.e. the minimal value of δ_{j}(s_{k}) among all φ_{j} which hold at s_{k}. Let u_{k} = δ_{j_{k}}(s_{k}), which implies that φ_{j_{k}} holds at s_{k}.

By C2, state s_{k+1} must satisfy φ_{j} for some j > 0, implying that s_{k+1} has a define rank u_{k+1}. Premise C2 requires that u_{k+1} ⪯ uk.

proceeding in this manner we obtain that every position i beyond k has a rank u_{i}, such that

u_{k} ⪰ u_{k+1} ⪰ u_{k+2} ⪰ · · · .

Since A is well-founded, there must exist a position r ≥ k such that

u_{r} = u_{r+1} = u_{r+2} = · · · .

Denote the value of this eventually-stable rank by u = u_{r}, and let j_{r} > 0 be the index of the assertion such that δ_{j_{r}}(s_{r}) = u.

Consider the value of the clock c_{j_{r}} at states s_{i}, i ≥ r. Since the rank never decreases beyond r, the value of c_{j_{1}} never decreases. Also, whenever a tick transition with increment Δ is taken, c_{j_{1}} increases (as do all clocks) by Δ. It follows that the master clock T cannot increase by more than B_{j_{r}}(s_{r}) − s_{r}[c_{j_{r}}] from its value at state s_{r}. This contradicts the fact that σ is a computation in which the master clock increases beyond all bounds.

We conclude that our assumption of the existence of a p-position not followed by any q-position is false. Consequently, if the premises of the rule hold then every p-position must be followed by a q-position, establishing the consequence of the rule.

The following example illustrates an application of rule cb-well.

Example 11. Consider program up-down presented in Fig. 28.

This program can be viewed as a generalization of program any-y in which, after terminating the while loop at ℓ_{0}, ℓ_{1}, process P_{1} proceeds to perform a second while loop at ℓ_{2}, ℓ_{3}, decrementing y until it reaches 0.

Assume, we assign the uniform time bounds [L, U] to all executable statements of program up-down, where our only information about L and U is given by

0 ≤ L < U < ∞.

We use rule cb-well to verify that program up-down terminates. This property can be expressed by the response formula

\underbrace{at_{−}ℓ_{0} ∧ at_{−}m_{0} ∧ x = y = t_{1} = t_{2} = T = 0}_{p} ⇒ � (\underbrace{at_{−}ℓ_{4} ∧ at_{−}m_{1}}_{q}).

x, y: integer where x = y = 0

[ \begin{matrix}ℓ_{0} : & while x = 0 do \\ ℓ_{1} : y := y + 1 \\ ℓ_{2} : & while y > 0 do \\ ℓ_{3} : y := y − 1 \\ ℓ_{4} : \end{matrix} ]  \left[{m_{0} : x := 1 \atop m_{1} :}\right]

− P_{1} −  − P_{2} −

Fig. 28. Program up-down.

As the well-founded domain, we take (ℕ^{2}, ≻), i.e., the domain of lexicographic pairs. As time bounds, we use B_{i}: U for all i = 1, …, 5. The auxiliary assertions, helpful clocks, and ranking functions are given by the following table:

φ_{0}: at_{−}ℓ_{4} ∧ at_{−}m_{1}  δ_{0}: 0
φ_{1}: at_{−}ℓ_{3} ∧ at_{−}m_{1} ∧ x = 1 ∧ y > 0 ∧ t_{1} ≤ U c_{1}: t_{1} δ_{1}: (1, 2y)
φ_{2}: at_{−}ℓ_{2} ∧ at_{−}m_{1} ∧ x = 1 ∧ y ≥ 0 ∧ t_{1} ≤ U c_{2}: t_{1} δ_{2}: (1, 2y + 1)
φ_{3}: at_{−}ℓ_{0} ∧ at_{−}m_{1} ∧ x = 1 ∧ y ≥ 0 ∧ t_{1} ≤ U c_{3}: t_{1} δ_{3}: 2
φ_{4}: at_{−}ℓ_{1} ∧ at_{−}m_{1} ∧ x = 1 ∧ y ≥ 0 ∧ t_{1} ≤ U c_{4}: t_{1} δ_{4}: 3

φ_{5}: at_{−}ℓ_{0,1} ∧ at_{−}m_{0} ∧ x = 0 ∧ y ≥ 0 ∧ t_{1} ≤ U ∧ t_{2} ≤ U

c_{5}: t_{1} δ_{5}: 4

We consider two instances of premise W2: transition ℓ_{2} taken from φ_{2} and transition ℓ_{3} taken from φ_{1}.

For the case of φ_{2}, premise W2 assumes the form

\underbrace{( \begin{matrix}y > 0 ∧ move(ℓ_{2}, ℓ_{3}) \\ ∨ \\ y ≤ 0 ∧ move(ℓ_{2}, ℓ_{4}) \end{matrix} ) ∧ pres(V −\{π\})}_{ρ_{ℓ_{2}}} ∧ \underbrace{at_{−}m_{1} ∧ x = 1 ∧ y ≥ 0 ∧ t_{1} ≤ U}_{φ_{2}}

→

⋯ ∨ ( \begin{matrix}\underbrace{at′_{−}ℓ_{3} ∧ at′_{−}m_{1} ∧ x′ = 1 ∧ y′ > 0 ∧ t′_{1} ≤ U}_{φ′_{1}} ∧ \underbrace{(1, 2y + 1) ≻ (1, 2y)}_{δ_{2}≻δ′_{1}} \\ ∨ \\ \underbrace{at′_{−}ℓ_{4} ∧ at′_{−}m_{1}}_{φ′_{0}} ∧ \underbrace{(1, 2y + 1) ≻ 0}_{δ_{2}≻δ′_{0}} \end{matrix} )

The implication uses the abbreviation

moveℓ_{i}, ℓ_{j}: ℓ_{i} ∈ π ∧ π′ = (π − {ℓ_{i}}) ∪ {ℓ_{j}}.

Note that move(ℓ_{i}, ℓ_{j}) implies at′_{−}ℓ_{j} and at′_{−}m_{1} = at_{−}m_{1}. Since ρ_{ℓ_{2}} implies y′ = y, the implication is obviously valid. In particular, due to

(1, 2y + 1) ≻ (1, 2y)  and  (1, 2y + 1) ≻ 0.

Premise R2 for φ_{1} and transition ℓ_{3} assumes the form

\underbrace{move(ℓ_{3}, ℓ_{2}) ∧ y′ = y − 1 ∧ pres(x, t_{1}, t_{2}, T)}_{ρ_{ℓ_{3}}} ∧

\underbrace{at_{−}ℓ_{3} ∧ at_{−}m_{1} ∧ x = 1 ∧ y > 0 ∧ t_{1} ≤ U}_{φ_{1}} →

⋯ ∨ (\underbrace{at′_{−}ℓ_{2} ∧ at′_{−}m_{1} ∧ x′ = 1 ∧ y′ ≥ 0 ∧ t′_{1} ≤ U}_{φ′_{2}} ∧ \underbrace{(1, 2y) ≻ (1, 2y′ + 1)}_{δ_{1}≻δ′_{2}})

Since ρ_{ℓ_{3}} implies y′ = y − 1, it is easy to verify that y > 0 implies y′ ≥ 0 and

(1, 2y′ + 1) = (1, 2(y − 1) + 1) = (1, 2y − 1) ≺ (1, 2y).

This establishes that the reponse property

at_{−}ℓ_{0} ∧ at_{−}m_{0} ∧ x = y = t_{1} = t_{2} = T = 0 ⇒ � (at_{−}ℓ_{4} ∧ at_{−}m_{1}).

is valid over program up-down.

5.7 Ranked Diagrams

The main ingredients of a proof by rule cb-well can be conveniently and effectively presented by a special type of verification diagrams that summarizes the auxiliary assertions, their helpful clocks and bounds, and their ranking functions, and display the possible transitions between the assertions.

We define a rabked diagram to be a directed labeled graph constructed as follows:

• Nodes in the graph are labeled by assertions. Each node is labeled by a pair of assertions: ϕ_{i} and β_{i}, for i = 0, …, m, and a ranking function δ_{i}. The assertion β_{i} has the form c_{i} ≤ B_{i}, where c_{i} ∈ C is a clock and B_{i} is a realvalued expression. We refer to the conjunction ϕ_{i} ∧ β_{i} as φ_{i}, and say that the node is labeled by the (combined) assertion φ_{i}. We often refer to nodes by the assertion φ_{i} labeling them. The node labeled by φ_{0} is called the terminal node and is graphically identified by being drawn with bold-face boundaries.

• Edges in the graph represent transitions between assertions. Each edge connects one assertion to another and is labeled by one or more transitions.

Verification Conditions Implied by a Ranked Diagram

Consider a nonterminal node labeled by assertion φ: ϕ ∧ β where the clockbound assertion is β: c ≤ B and the ranking function is δ. Let τ ∈ T_{T} be a transition and let φ_{1}, …, φ_{k}, k ≥ 0, be the successors of φ by edges labeled with τ (possibly including φ itself). With each such node and transition, we associate the following verification condition:

\begin{matrix}ρ_{τ} ∧ φ → (φ′ ∧ δ′ = δ ∧ c ≤ c′ ≤ B′ ≤ B) ∨ (φ′ ∧ δ ≻ δ′) ∨ \\ (φ′_{1} ∧ δ ≻ δ′_{1}) ∨ ⋯ ∨ (φ′_{k} ∧ δ ≻ δ′_{k}). \end{matrix}

In particular, if k = 0 (i.e., φ has no τ-successors), the associated verification condition is

ρ_{τ} ∧ φ → (φ′ ∧ δ′ = δ ∧ c ≤ c′ ≤ B′ ≤ B) ∨ (φ′ ∧ δ ≻ δ′).

Valid Ranked Diagrams

A Ranked diagram is said to be valid over cts Φ (Φ-valid for short) if all the verification conditions associated with the diagram are Φ-state valid.

The consequences of having a valid chain diagram are stated in the following claim:

Claim 7 If D is a Φ-valid ranked diagram with nodes φ_{0}, …, φ_{m}, then

Φ ⊧ ⋁_{j=0}^{m} φ_{j} ⇒ � φ_{0}

If, in addition, φ_{0} = q and

W1: p → ⋁_{j=0}^{m} φ_{j},

then we can conclude:

Φ ⊧ p ⇒ � q.

Example 12. In Fig. 29, we present a ranked diagram which establishes that the response property

at_{−}ℓ_{0} ∧ at_{−}m_{0} ∧ x = y = t_{1} = t_{2} = T = 0 ⇒ � (at_{−}ℓ_{4} ∧ at_{−}m_{1}).

is valid over program up-down.

Observe that the β assertions for nodes ϕ_{1}-ϕ_{4} appear at the head of the compound nodes containing these nodes, as part of the encapsulation conventions.

5.8 From Waiting-for to Response Properties

In many useful cases, we can infer response formulas from a waiting-for formula of a particular form.

Rule W→R, presented in Fig. 30, infers a response formula from a waiting-for formula of a special form.

ϕ_{5}: at_{−}ℓ_{0,1} ∧ at_{−}m_{0} ∧ x = 0 ∧ y ≥ 0, β: t_{2} ≤ 5, δ: 4 m_{0} ϕ_{0}: at_{−}ℓ_{4} ∧ at_{−}m_{1},  δ: 0 t_{2}, T ≥ 0, 0 ≤ t_{1} ≤ U ϕ_{4}: at_{−}ℓ_{1},  δ: 3 ℓ_{1} ϕ_{3}: at_{−}ℓ_{0},  δ: 2 ℓ_{0} ℓ_{2} ϕ_{2}: at_{−}ℓ_{2},  δ: (1, 2y + 1) ϕ_{1}: at_{−}ℓ_{3} ∧ y > 0,  δ: (1, 2y) at_{−}m_{1}, x = 1, y ≥ 0,  β: t_{1} ≤ U at_{−}m_{1}, x = 1, y ≥ 0,  β: t_{1} ≤ U ℓ_{1}  ℓ_{2}

Fig. 29. A ranked diagram, establishing the formula at_{−}ℓ_{0} ∧ at_{−}m_{0} ∧ x = y = t_{1} = t_{2} = T = 0 ⇒ � (at_{−}ℓ_{4} ∧ at_{−}m_{1})

Justification: Assume that the waiting-for premise is Φ-valid. Consider a Φ-computation σ, and a p-position j ≥ 0 in σ. By the waiting-for formula, j initiates an interval, all of whose positions satisfy q ∧ T_{a} ≤ B, which either extends to infinity or is terminated by an r-position. Since σ is a computation, T must grow beyond all values and cannot remain bounded by a + b (T_{a} ≤ b is equivalent to T ≤ a + b) at all positions. It follows that j must be followed by an r-position.

Example 13. Consider the spl_{T} program up-down_{[1,5]}, which is program up-down with time bounds [1,5] uniformly assigned to all executable statements.

We use rule W→R to verify that the response formula

at_{−}ℓ_{0} ∧ at_{−}m_{0} ∧ x = y = T_{a} = 0 ⇒ � (at_{−}ℓ_{4} ∧ at_{−}m_{1} ∧ T_{a} ≤ 50)

is valid over program up-down_{[1,5]}.

In Fig. 31, we present a waiting diagram which establisehs the up-down_{[1,5]}-

For assertions p, q, and r, and rigid expression B, p ⇒ (q ∧ T_{a} ≤ B) W r p ⇒ � r

Fig. 30. Rule W→R (from waiting-for to response formulas).

validity of the waiting-for formula

at_{−}ℓ_{0} ∧ at_{−}m_{0} ∧ x = y = T_{a} = 0 ⇒ (T_{a} ≤ 50) W (at_{−}ℓ_{4} ∧ T_{a} ≤ 50)

Note that the assertion describing the initial state does not specify initial values for either t_{1} or t_{2}. To show that the waiting diagram is valid, we rely on the following invariant:

� ((at_{−}ℓ_{0} → 0 ≤ t_{1} ≤ 5) ∧ (at_{−}m_{0} → 0 ≤ t_{2} ≤ 5)).

This invariant can be separately established, using the methods of Section 4.

5.9 Are Rules cb-chain and cb-well Really Necessary?

Rule W→R enables the derivation of a response property from a timed waitingfor property, which can be established using rule wait. Rule wait (and its equivalent formulation in terms of waiting diagrams) is, in principle, simpler than either rule cb-chain or rule cb-well, because it does not require the identification of explicit time bounds or ranking functions as auxiliary constructs.

In view of this, a naturally rising question is why do we need the responsespecific rules cb-chain and cb-well. Isn’t rule W→R adequate for establishing all response properties of interest?

We provide two answers to this question. The first answer is that there are some response properties that cannot be established through timed waiting-for properties.

To support this point, consider again program up-down but with general (uniform) time bounds, [L, U], such that 0 ≤ L ≤ U < ∞. For all cases that L > 0, we can essentially repeat the analysis done in Example 13, and establish the waiting-for formula

at_{−}ℓ_{0} ∧ at_{−}m_{0} ∧ x = y = T_{a} = 0 ⇒ (T_{a} ≤ B) W (at_{−}ℓ_{4} ∧ T_{a} ≤ B),

where

B = (6 + 2 ⌊\frac{U}{2L}⌋)U.

Applying rule W→R to this formula, one can infer the response formula

at_{−}ℓ_{0} ∧ at_{−}m_{0} ∧ x = y = T_{a} = 0 ⇒ � (at_{−}ℓ_{4} ∧ T_{a} ≤ B),

m_{0} ℓ_{0} ℓ_{2} at_{−}m_{1}, x = 1, y ≤ 3 at_{−}ℓ_{2} ∧ T_{a} ≤ 45 − 10y + t_{1} ≤ 50 − 10y at_{−}ℓ_{3} ∧ y > 0 ∧ T_{a} ≤ 50 − 10y + t_{1} ≤ 55 − 10y at_{−}ℓ_{4} ∧ T_{a} ≤ 50 ℓ_{1} y ≥ 0, T_{a} ≥ 0, 0 ≤ t_{1} ≤ 5, 0 ≤ t_{2} ≤ 5 ℓ_{1} at_{−}m_{1}, x = 1 at_{−}ℓ_{1} ∧ y ≤ 2 ∧ T_{a} ≤ 5 + t_{1} ≤ 10 at_{−}ℓ_{0} ∧ y ≤ 3 ∧ T_{a} ≤ 10 + t_{1} ≤ 15 at_{−}m_{0}, x = 0, T_{a} ≤ t_{2} ≤ 5 at_{−}ℓ_{0} ∧ (y = 0 ∨ 2y + t_{1} ≤ T_{a} + 1) at_{−}ℓ_{1} ∧ 2y + t_{1} ≤ T_{a} ℓ_{1}  ℓ_{2}

Fig. 31. A waiting diagram, establishing the formula at_{−}ℓ_{0} ∧ at_{−}m_{0} ∧ x = y = T_{a} = 0 ⇒ (T_{a} ≤ 50) W (at_{−}ℓ_{4} ∧ T_{a} ≤ 50)

guranteeing termination within B time units.

One can see that as L gets closer to 0, the bound on termination time gets larger. It is therefore not surprising that when L = 0, there is no bound on the time it takes the program to terminate. Yet, all computations of this program eventually lead to the termination state at_{−}ℓ_{4}. Thus, termination of program up-down in the case of L = 0 is a response property that cannot be verified using rule W→R. On the other hand, in Example 11, we established termination of up-down, using rule cb-well, in a proof that is valid for all L ≥ 0. This illustrates the case of a response property that cannot be proven by rule W→R, but is provable by rule cb-well.

As the second answer justifying the introduciton of rule cb-well, we propose to compare the verification diagram of Fig. 29 with that of Fig. 31, both establishing termination of up-down for the time bounds [1, 5] (Fig. 29 actually established it for general [L, U]). It is obvious that diagram 31 require a much more detailed analysis of the precise time interval which we can spend at each of the diagram nodes. In comparison, the diagram of Fig. 29 said very litle about these time intervals. The only timing information included in this diagram was that the time spent at each of the nodes is bounded by U. Thus, when we need or are ready to conduct a very precise analysis of the time intervals spent at each node, it makes sense to use waiting diagrams and rule W→R. If, on the other hand, we are content with less quantitative anlysis, and are only interested in the qualitative fact that eventually q will occur (which is the essence of the � termporal operator), we may use rule cb-well or rule cb-chain. These rules may be conceptually more complicated than rule wait, but their application calls for a simpler analysis of the program.

6 Proving that a cts is Non-Zeno

It is by now a widely accepted notion that the only interesting real-time systems are those which obey the non-zeno restriction. One of the reasons is that, since we only consider time-divergent runs as computations, a possibly-zeno system may contain components that will never be accessed in a computation. In some sense, these components are redundant to the description of the system and their inclusion is superfluous and often confusing and misleading. Non-zeno systems, on the other hand, contain no such redundancy, since every accessible state also appears in some computation.

In view of the significance of the non-zeno restriction, it is important to be able to verify that an arbitrary given cts is non-zeno.

In many cases, there are simple sufficient conditions which guarantee that the system is non-zeno. One of the most important case is the following:

Claim 8 Let P be an spl_{T} program in which the upper bound assigned to each executable statement is positive. Then F_{P}, the cts corresponding to P, is a non-zeno system.

Justification Let U_{m} > 0 be the minimal upper bound. Consider a finite run r: s_{0}, …, s_{k}. We wish to show that r can be extended into a computation.

The recipe for extending r considers the last reached state s (starts at s = s_{k} and decides to apply the next transition as follows:

• If the tick transition is enabled on s, take the tick transition with increment Δ > 0, which is the maximal Δ ≤ 1 satisfying s ⊧ Ω(Δ).

• If the tick transition is disabled on s, it must be blocked by one of the processes, say P_{i}, whose clock t_{i} has reached the upper bound of some transition τ of P_{i} which is currently enabled. In this case, take this ripe transition τ.

It is not difficult to check that an accessible state in a clocked transition systems derived from a program with positive upper bounds always has at least one extended transition enabled on it. Thus, the described recipe produces an infinite run. This observation hinges on the revised transition relation we associated with the wait statement.

It only remains to check that the infinite run produced by this recipe is timedivergent and, hence, is a computation. By considering the different possibilities, we observe that two cases are possible.

In one case, we eventually reach a state s such that s ⊧ Ω(Δ), for every Δ > 0. In this case, once we reach this s, we continue to take tick steps with Δ = 1.

In the remaining case, for every reached state s_{i}, there exists a limit Δ_{i} such that s_{i} ⊧ Ω(Δ) for no Δ > Δ_{i}. In this case, our construction must take infinitely many untimed transitions, i.e., transitions τ ≠ tick. Note that each such transition resets one of the clocks to 0. It follows that the construction of the infinite run causes at least one of the clocks, say t_{i}, to be reset to 0 infinitely many times. It is not difficult to see that between two consecutive resets of clock t_{i}, time must progress by at least U_{m}. It follows that time has progressed infinitely many time by the amount U_{m} > and, therefore, the run is time-divergent.

6.1 A Rule for Establishing Non-Zenoness

While Claim 8 settles the question of non-zenoness for many useful cases, there are additional cases which require different methods. The claim was established for the simpler case that the upper bounds assigned to transitions were positive constants. It can easily be generalized to state-dependent upper bounds which are bounded from below by a positive constant. However, this still does not cover all possible cases. For example, cts Φ_{4} presented in Fig. 32, is a non-zeno system, even though, the upper bounds of the transition connecting ℓ_{0} to itself have no lower bound.

ℓ_{0}: t_{1} < \frac{1}{\sqrt{y}} (y, t_{1}) := (y + 1, 0)

y: integer where y = 1 t_{1}, T: real where t_{1} = T = 0 Fig. 32. A nonzeno cts Φ_{4} with upper bounds tending to 0.

The general strategy we propose for proving that a given cts Φ is non-zeno is summarized in rule nonz, presented in Fig. 33.

For assertion φ,

N1. Φ ⊧ φ

N2. Φ ⊧ AG(φ ∧ V = V_{0} ∧ T_{a} = 0 → EF (T_{a} > 0))

Φ is non-zeno

Fig. 33. Rule nonz (Φ is a non-zeno cts).

The rule uses an auxiliary assertion φ. Premise N1 requires that φ is Φ-state valid, and can be proven using rule acc.

Premise N2 belongs to the realm of branching-time temporal logic, which is different from the linear-time temporal framework we have been consistently using in this paper. It has long been observed that the property of being nonzeno cannot be formulated in linear-time tl and needs branching-time tl for its precise formulation. In a recent paper ([Lam95]), Lamport makes this observation but suggests a method by which properties such as non-zenoness can still be verified in a linear framework. We prefer to use the branching-time logic ctl([EC82]) for formulating the required property, as in premise N2, and present a single proof rule which is adequate to establish ctl formulas such as the one presented in N2. A deductive system for verifying the main ctl properties appeared in [BAMP83]. A more comprehensive deductive system for ctl was recently proposed in [FG95].

6.2 Verifying Possibility Formulas

A possibility formula is a ctlformula of the form

AG(p → EF q),

for assertions p and q. Without entering into the individual meaning of the ctl temporal operators AG and EF, we say that the possibility formula AG(p → EF q) is valid over cts Φ (Φ-valid) if

For every accessible p-state s, there exists a run segment s=s_{1}, …, s_{k} leading from s to a q-state s_{k}.

We write

Φ ⊧ AG(p → EF q)

to indicate that the possibility formula AG(p → EF q) is Φ-valid.

For assertions p, q, and φ_{0} = q, φ_{1}, …, φ_{m},

transitions τ_{1}, …, τ_{m} ∈ T_{T},

functions Next_{1}, …, Next_{m}: Σ ↦ Σ, a well-founded domain (A, ≻), and ranking functions δ_{0}, …, δ_{m}: Σ ↦ A,

G1. p → ⋁_{j=0}^{m} φ_{j}

The following premise holds for i = 1, …, m

G2. φ_{i} ∧ V′ = Next_{i} → ρ_{τ_{i}} ∧ ⋁_{j=0}^{m}(φ′_{j} ∧ δ_{i} ≻ δ′_{j})

Φ ⊧ AG(p ⇒ EF q)

Fig. 34. Rule g-poss (Φ validity of a possibility formula).

In Fig. 34, we present rule poss which is sound and complete for proving the Φ-validity of a possibility formula.

The rule requires finding auxiliary assertions φ_{i}, functions Next_{i}: Σ ↦ Σ, and transitions τ_{i}, i = 1, …, m, a well-founded domain (A, ≻), and ranking functions δ_{i}: S ↦ A. Each assertion φ_{i} is associated with the transition τ_{i} that is helpful at positions satisfying φ_{i}, with a function Next_{i} that selects a successor state, and with its own ranking function δ_{i}. We have presented the successor-selection functions Next_{i} as mapping states to states but, in fact, they map s[V], i.e., the values of the system variables in state s, to s′[V], the values of the system variables in a successor state s′.

Premise G1 requires that every p-position satisfies one of φ_{0}, …, φ_{m}.

Premise G2 considers a φ_{i}-state s and a state s̃ such that s̃[V] = s[V′] = Next_{i}, for some i = 1, …, m. The premise requires that s̃ is a τ_{i}-successor of s which satisfies φ_{j}, for some j = 0, …, m and has a rank lower than that of s. Justification Let s be a p-state. We will show that there exists a run segment s=s_{1}, …, s_{k} which leads from s to a q-state. By premise G1, s = s_{1} must satisfy φ_{j}, for some j = 0, …, m. Let j_{1} be the minimal j such that s ⊧ φ_{j}. If j = 0, we are done, since s_{1} satisfies φ_{0} = q.

Otherwise, j_{1} > 0 and let u_{1} = δ_{j_{1}}(s_{1}). Let s_{2} be any state such that s_{2}[V] = Next_{j_{1}}(s_{1}[V]). By premise G2, s_{2} is a τ_{j_{1}}-successor of s_{1}, satisfies φ_{j_{2}} for some j_{2} ∈ {0, …, m}, and a rank u_{2} = δ_{j_{2}}(s_{2}) ≺ u_{1}. If j_{2} = 0, we are done. Otherwise, we take s_{3} to be some Next_{j_{2}}-selected successor of s_{2}, and so on.

This construction can terminate when we reach some k such that j_{k} = 0. If it does no terminate, we generate an infinite descending sequence

u_{1} ≻ u_{2} ≻ · · · .

This is impossible due to the well-foundedness of A. We conclude that the construction must terminate in a state s_{k} satisfying φ_{0} = q.

Example 14. We illustrate the application of rule g-poss for proving that the possibility formula

AG(\underbrace{at_{−}ℓ_{0,1} ∧ T_{a} = 0}_{p} → EF (\underbrace{T_{a} ≥ 1}_{q}))

is valid over cts Φ_{5}, presented in Fig. 35.

T: real where t_{1} = T = 0

ℓ_{0}: T < 1  τ  ℓ_{1}:

Fig. 35. A nonzeno cts Φ_{5}.

Observe that transition τ, the only transition in Φ_{5}, has two successors. One satisfying at_{−}ℓ_{0} and the other satisfying at_{−}ℓ_{1}.

To apply rule g-poss, we take (ℕ, >) (the domain of the natural numbers) as the well-founded domain. The auxiliary assertions, helpful transitions, successorselection functions, and ranking functions are given by the following table:

φ_{0}: T_{a} ≥ 1  τ_{0}: tick Next_{0}: (π′ : 1, T′ : T + 1) δ_{0}: 0
φ_{1}: at_{−}ℓ_{1} ∧ T_{a} ≥ 0 τ_{1}: tick Next_{1}: (π′ : 1, T′ : T + 1) δ_{1}: 1
φ_{2}: at_{−}ℓ_{0} ∧ T_{a} ≥ 0 τ_{2}: τ  Next_{2}: (π′ : 1, T′ : T)  δ_{2}: 2

This choice of constructs, corresponds to a strategy of constructing a run segment in which time will progress by at least 1. According to this strategy, if we are at ℓ_{0}, we choose to take transition τ and choose a τ-successor state satisfying at_{−}ℓ_{1}. If we are at ℓ_{1}, we choose to take the tick transition with time increment 1.

It is not difficult to check that all premises of rule g-poss are satisfied by this choice of constructs.

It follows that the possibility formula

AG(at_{−}ℓ_{0,1} ∧ T_{a} = 0 → EF (T_{a} ≥ 1))

is Φ_{5}-valid.

Systems with Deterministic Transitions

Rule g-poss is very general and can be shown to be complete for proving possibilities properties of all clocked transition systems. However, there is a big family of systems which can be handled by a rule which call for identification of simpler constructs.

A transition τ of a cts is called deterministic if all the τ-successors of an accessible state assign the same values to the system variables. That is, if we restrict our attention to the values of the system variables, each accessible state has at most one τ-successor. We say that a cts Φ is transition-deterministic (Φ is a td-ctss for short) if all of its (untimed) transitions are deterministic. All the systems we have presented in this paper, excluding Φ_{5}, are transitiondeterministic.

Consider a td-ctss Φ. Assume that we wish to construct the successorselection function Next_{i} corresponding to assertion φ_{i}, where τ_{i} ≠ tick. Since τ_{i} is deterministic, Next_{i} is uniquely determined, and its explicit specification is redundant. The situation is different with the tick transition, which may have (uncountably) many successors, each corresponding to a different value of the time increment Δ. However, once we specify the value of Δ, the successor of a tick transition is also uniquely determined up to differences in non-system variables.

Thus, instead of specifying a complete successor function, specifying the values of all system variables in the successor state, it is sufficient to specify the time increment Δ_{i} associated with the successor. For uniformity, we specify values of Δ_{i} also for untimed transitions, but then we ensure that Δ_{i} = 0.

This leads to rule poss (Fig. 36) which is adequate for proving possibility properties of every td-ctss. Rule poss has more premises than rule g-poss but it requires the identification of simpler constructs, and the premises are easier to verify.

Note that rule poss splits premise G2 of rule g-poss into two premises. Premise P2 guarantees that the (unique) successor of a φ_{i}-state corresponding to the identification of the helpful transition τ_{i} and the time increment Δ_{i} (if it exists), satisfies some φ_{j} with a lower rank. Premise P3 guarantees that each φ_{i} state does have a successor corresponding to τ_{i} and Δ_{i}. The premise is split into the case of the tick transition (sub-premise P3t) and the case of all other untimed transitions (sub-premise P3n). Sub-premise P3t requires that φ_{i} imply Ω, the enabling condition of of transition tick, with the specified Δ_{i}. Sub-premise P3n requires that Δ_{i} = 0 and that φ_{i} implies the enableness of τ_{i}.

Example 15. We illustrate the use of rule poss for proving that the possibility formula

AG(\underbrace{at_{−}ℓ_{0} ∧ 1 ≤ b = y ∧ 0 ≤ t_{1} ≤ \frac{1}{\sqrt{y}} ∧ 0 = T_{a}}_{p} → EF (\underbrace{T_{a} ≥ 1}_{q}))

is valid over cts Φ_{4}.

For assertions p, q, and φ_{0} = q, φ_{1}, …, φ_{m},

transitions τ_{1}, …, τ_{m} ∈ T_{T},

time increments Δ_{1}, …, Δ_{m} ≥ 0, a well-founded domain (A, ≻), and ranking functions δ_{0}, …, δ_{m}: Σ ↦ A,

P1. p → ⋁_{j=0}^{m} φ_{j}

The following premises hold for i = 1, …, m

P2. ρ_{τ_{i}} ∧ T′ = T + Δ_{i} ∧ φ_{i} → ⋁_{j=0}^{m}(φ′_{j} ∧ δ_{i} ≻ δ′_{j})

P3. If τ_{i} = tick then

P3t. φ_{i} → Ω(Δ_{i}) Otherwise

P3n. φ_{i} → Δ_{i} = 0 ∧ En(τ_{i})

Φ ⊧ AG(p ⇒ EF q)

Fig. 36. Rule poss (Φ validity of a possibility formula).

Note that cts Φ_{4} has a single untimed transition, to which we refer as τ_{00}. As the well-founded domain, we take (ℕ^{2}, ≻), the domain of lexicographic

pairs. The auxiliary assertions, helpful transitions, time increments, and ranking functions are given by the following table:

φ_{0}: T_{a} ≥ 1 τ_{0}: τ_{00} Δ_{0}: 0  δ_{0}: 0

φ_{1}: at_{−}ℓ_{0} ∧ 1 ≤ b ≤ y ≤ 2b + 1 ∧ t_{1} = 0 ∧ \frac{y−b−1}{\sqrt{2b+1}} ≤ T_{a} < 1

τ_{1}: tick Δ_{1}: \frac{1}{\sqrt{y}}  δ_{1}: (|2b + 1 − y|, 2)

φ_{2}: at_{−}ℓ_{0} ∧ 1 ≤ b ≤ y ≤ 2b + 1 ∧ t_{1} = \frac{1}{\sqrt{y}} ∧ \frac{y−b}{\sqrt{2b+1}} ≤ T_{a} < 1

τ_{2}: τ_{00} Δ_{2}: 0  δ_{2}: (|2b + 1 − y|, 1)

φ_{3}: at_{−}ℓ_{0} ∧ 1 ≤ b ≤ y ≤ 2b + 1 ∧ 0 < t_{1} < \frac{1}{\sqrt{y}} ∧ 0 ≤ T_{a} < 1

τ_{3}: tick Δ_{3}: \frac{1}{\sqrt{y}} − t_{1} δ_{3}: 2b + 2

The idea behind this selection is the following. Starting in a state at which y = b ≥ 1 and 0 < t_{1} < \frac{1}{\sqrt{y}} (described by assertion φ_{3}), we first step time with an increment \frac{1}{\sqrt{y}} − t_{1}, this will get us to a state in which t_{1} = \frac{1}{\sqrt{y}} (described by φ_{2}). From this point on, we alternate between taking untimed transition τ_{00} which increments y by 1 but preserves time, and taking transition tick, which increments time by \frac{1}{\sqrt{y}} but preserves the value of y. We repeat this couple of steps at most b + 1 times, letting y increase from b to 2b + 1. Since the time step in each round is decreasing, the total time increase is not less than b + 1 times the last time increment which is \frac{1}{\sqrt{2b+1}}. Thus the total time increase is not less than

\frac{b + 1}{\sqrt{2b + 1}} ≥ 1,

where the inequality holds for every b ≥ 1.

This informal argument can be formalized by checking that all premises of rule poss are state valid for the specified selection of the auxiliary assertions, helpful transitions, time increments, and well-founded ranking.

This establishes that the possibility formula

AG(at_{−}ℓ_{0} ∧ 1 ≤ b = y ∧ 0 ≤ t_{1} ≤ \frac{1}{\sqrt{y}} ∧ 0 = T_{a} → EF (T_{a} ≥ 1))

is valid over cts Φ_{4}.

6.3 Possibility Diagrams

Proofs according to rule poss can be succinctly represented by possibility diagrams.

A possibility diagram is a directed labeled graph constructed as follows:

• Nodes in the graph are labeled by assertions φ_{0}, …, φ_{m}. We will often refer to a node by the assertion labeling it. In addition to the assertion, each node is also labeled by a ranking function δ. The node labeled by φ_{0} is called the terminal node and is graphically identified by being drawn with bold-face boundaries.

• Edges in the graph represent transitions between assertions. Each edge is labeled by the name of an untimed transition in the program or by a label of the form tick(Δ). We refer to an edge labeled by τ (including the case that τ = tick) as a τ-edge. All edges departing from the same node must have the same label. Every non-terminal node must have an edge departing from it. No edges depart form the terminal node.

• Some of the nodes are designated as initial nodes. They are annotated by an entry arrow.

Verification Conditions Implied by a Chain Diagram

Consider a nonterminal node labeled by assertion φ and ranking function del. Let φ_{1}, …, φ_{k}, k > 0, be the successors of φ by edges departing from φ (possibly including φ itself). With each such node, we associate the following verification condition:

• If the label of all edges departing from φ is tick(Δ), then we require the following verification conditions to hold:

\begin{matrix}P2. & ρ_{tick} ∧ T′ = T + Δ ∧ φ → (φ′_{1} ∧ δ ≻ δ′_{1}) ∧ ⋯ ∧ (φ′_{k} ∧ δ ≻ δ′_{k}) \\ P3t. & φ → Ω(Δ) \end{matrix}

• If the label of all edges departing from φ is τ ≠ tick, then we require the following verification conditions to hold:

\begin{matrix}P2. & ρ_{τ} ∧ T′ = T ∧ φ → (φ′_{1} ∧ δ ≻ δ′_{1}) ∧ ⋯ ∧ (φ′_{k} ∧ δ ≻ δ′_{k}) \\ P3n. & φ → En(τ) \end{matrix}

Valid Possibility Diagrams

A possibility diagram is said to be valid over cts Φ (Φ-valid for short) if all the verification conditions associated with the diagram are P -state valid.

The consequences of having a valid chain diagram are stated in the following claim:

Claim 9 If D is a Φ-valid possibility diagram with nodes φ_{0}, …, φ_{m}, then

Φ ⊧ AG( ⋁_{j=0}^{m} φ_{j} → EF φ_{0})

If, in addition, φ_{0} = q, and

p → ⋁_{j=0}^{m} φ_{j},

then we can conclude:

Φ ⊧ AG(p → EF q).

Example 16. In Fig. 37, we present a waiting diagram that establishes the possibility property

AG(at_{−}ℓ_{0} ∧ 1 ≤ b = y ∧ 0 ≤ t_{1} ≤ \frac{1}{\sqrt{y}} ∧ 0 = T_{a} → EF (T_{a} ≥ 1))

for system Φ_{4}.

6.4 Proving that Φ_{4} is Non-Zeno

We conclude this discussion by applying rule nonz to show that cts Φ_{4} is nonzeno.

As the assertion φ required by rule nonz, we take

φ: at_{−}ℓ_{0} ∧ y ≥ 1 ∧ 0 ≤ t_{1} ≤ \frac{1}{\sqrt{y}} .

It is not difficult to show by rule acc that φ is Φ_{4}-state valid. This establishes premise N1 of rule nonz.

For premise N2 of nonz, we have to verify the possibility formula

AG(at_{−}ℓ_{0} ∧ y ≥ 1 ∧ 0 ≤ t_{1} ≤ \frac{1}{\sqrt{y}} ∧ y = b ∧ T_{a} = 0 → EF (T_{a} ≥ 1)).

This is essentially done in Example 15.

We conclude that cts Φ_{4} is non-zeno.

at_{−}ℓ_{0}, 1 ≤ b ≤ y ≤ 2b + 1, t_{1} ≥ 0, 0 ≤ T_{a} < 1 φ_{3}: 0 < t_{1} < \frac{1}{\sqrt{y}}  δ: 2b + 2 tick(\frac{1}{\sqrt{y}} − t_{1}) φ_{2}: t_{1} = \frac{1}{\sqrt{y}} ∧ T_{a} ≥ \frac{y−b}{\sqrt{2b+1}}  δ: (|2b + 1 − y|, 1) φ_{0}: T_{a} ≥ 1 δ: 0 φ_{1}: t_{1} = 0 ∧ T_{a} ≥ \frac{y−b−1}{\sqrt{2b+1}}  δ: (|2b + 1 − y|, 2) τ_{00} tick(\frac{1}{\sqrt{y}}) tick(\frac{1}{\sqrt{y}})

Fig. 37. A possibility diagram, establishing the formula AG(at_{−}ℓ_{0} ∧ 1 ≤ b = y ∧ 0 ≤ t_{1} ≤ \frac{1}{\sqrt{y}} ∧ 0 = T_{a} → EF (T_{a} ≥ 1))

Conclusions

In this paper we have presented the new real-time model of clocked transition system (cts). This model can be viewed as an extension of the timed automata model [AD94]. In addition to algorithmic verification of finite-state systems, the cts model can also support deductive verification. In this paper, we have restricted our attention to the verification of safety properties, and have shown a reduction from a cts to an fts, a reduction that preserves all the safety properties of the original system. This reduction allows us to use methodologies and tools developed for the fts model to verify safety properties of real-time systems. In a similar way, we have shown a reduction from the phase transition system model to the fts model, enabling the reuse of fts-verification methods for establishing safety properties of hybrid systems.

Acknowledgment

We gratefully acknowledge the careful reading and critical comments of Oded Maler, Henny Sipma, and Tomás Uribe.

References

[AD94] R. Alur and D.L. Dill. A theory of timed automata. Theor. Comp. Sci., 126:183–235, 1994.

[AH89] R. Alur and T.A. Henzinger. A really temporal logic. In Proc. 30th IEEE Symp. Found. of Comp. Sci., pages 164–169, 1989.

[AH92] R. Alur and T. Henzinger. Logics and models of real time: A survey. In J.W. de Bakker, C. Huizing, W.P. de Roever, and G. Rozenberg, editors, Proceedings of the REX Workshop “Real-Time: Theory in Practice”, volume 600 of Lect. Notes in Comp. Sci., pages 74–106. Springer-Verlag, 1992.

[AL94] M. Abadi and L. Lamport. An old-fashioned recipe for real time. ACM Trans. Prog. Lang. Sys., 16(5):1543–1571, 1994.

[BAMP83] M. Ben-Ari, Z. Manna, and A. Pnueli. The temporal logic of branching time. Acta Informatica, 20:207–226, 1983.

[BH81] A. Bernstein and P. K. Harter. Proving real time properties of programs with temporal logic. In Proceedings of the Eighth Symposium on Operating Systems Principles, pages 1–11. ACM, 1981.

[EC82] E.A. Emerson and E.M. Clarke. Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comp. Prog., 2:241–266, 1982.

[FG95] L. Fix and O. Grumberg. Verificaiton of temporal properties. to appear in Logic and Computation, 1995.

[Har87] D. Harel. Statecharts: A visual formalism for complex systems. Sci. Comp. Prog., 8:231–274, 1987.

[Hen92] T.A. Henzinger. Sooner is safer than later. Info. Proc. Lett., 43(3):135–142, 1992.

[HMP94] T. Henzinger, Z. Manna, and A. Pnueli. Temporal proof methodologies for timed transition systems. Inf. and Comp., 112(2):273–337, 1994.

[KdR85] R. Koymans and W.-P. de Roever. Examples of a real-time temporal logic specifications. In B.D. Denvir, W.T. Harwood, M.I. Jackson, and M.J. Wray, editors, The Analysis of Concurrent Systems, volume 207 of Lect. Notes in Comp. Sci., pages 231–252. Springer-Verlag, 1985.

[Koy90] R. Koymans. Specifying real-time properties with metric temporal logic. Real-time Systems, 2(4):255–299, 1990.

[KVdR83] R. Koymans, J. Vytopyl, and W.-P. de Roever. Real-time programming and asynchronous message passing. In Proc. 2nd ACM Symp. Princ. of Dist. Comp., pages 187–197, 1983.

[Lam95] L. Lamport. Proving possibiity properties. Technical Report 137, Digital Equipment Corporation, Systems Research Center, Palo Alto, July 1995.

[MAB^{+}94] Z. Manna, A. Anuchitanukul, N. Bjørner, A. Browne, E. Chang, M. Colón, L. De Alfaro, H. Devarajan, H. Sipma, and T. Uribe. STeP: The Stanford Temporal Prover. Technical Report STAN-CS-TR-94-1518, Dept. of Comp. Sci., Stanford University, Stanford, California, 1994.

[MMP92] O. Maler, Z. Manna, and A. Pnueli. From timed to hybrid systems. In J.W. de Bakker, C. Huizing, W.P. de Roever, and G. Rozenberg, editors, Proceedings of the REX Workshop “Real-Time: Theory in Practice”, volume 600 of Lect. Notes in Comp. Sci., pages 447–484. Springer-Verlag, 1992.

[MP91a] Z. Manna and A. Pnueli. Completing the temporal picture. Theor. Comp. Sci., 83(1):97–130, 1991.

[MP91b] Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1991.

[MP93] Z. Manna and A. Pnueli. Models for reactivity. Acta Informatica, 30:609– 678, 1993.

[MP94] Z. Manna and A. Pnueli. Temporal verification diagrams. In T. Ito and A. R. Meyer, editors, Theoretical Aspects of Computer Software, volume 789 of Lect. Notes in Comp. Sci., pages 726–765. Springer-Verlag, 1994.

[MP95] Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995.

[MT90] F. Moller and C. Tofts. A temporal calculus of communicating systems. In J.C.M. Baeten and J.W. Klop, editors, Proceedings of Concur’90, volume 458 of Lect. Notes in Comp. Sci., pages 401–415. Springer-Verlag, 1990.

[NSY92] X. Nicollin, J. Sifakis, and S. Yovine. From ATP to timed graphs and hybrid systems. In J.W. de Bakker, C. Huizing, W.P. de Roever, and G. Rozenberg, editors, Proceedings of the REX Workshop “Real-Time: Theory in Practice”, volume 600 of Lect. Notes in Comp. Sci., pages 549–572. Springer-Verlag, 1992.

[Ost90] J.S. Ostroff. Temporal Logic of Real-Time Systems. Advanced Software Development Series. Research Studies Press (John Wiley & Sons), Taunton, England, 1990.

[Pnu92] A. Pnueli. How vital is liveness? In W.R. Cleaveland, editor, Proceedings of Concur’92, volume 630 of Lect. Notes in Comp. Sci., pages 162–175. Springer-Verlag, 1992.

[SBM92] F. B. Schneider, B. Bloom, and K. Marzullo. Putting time into proof outlines. In J.W. de Bakker, C. Huizing, W.P. de Roever, and G. Rozenberg, editors, Proceedings of the REX Workshop “Real-Time: Theory in Practice”, volume 600 of Lect. Notes in Comp. Sci., pages 618–639. Springer-Verlag, 1992.

[Sif91] J. Sifakis. An overview and synthesis on timed process algebra. In K.G. Larsen and A. Skou, editors, 3rd Computer Aided Verification Workshop, volume 575 of Lect. Notes in Comp. Sci., pages 376–398. Springer-Verlag,