BRICS RS-94-43 Aceto & Jeffrey: A Complete Axiomatization of Timed Bisimulation

BRICS

Basic Research in Computer Science

A Complete Axiomatization of Timed Bisimulation for a Class of Timed Regular Behaviours

(Revised Version)

Luca Aceto Alan Jeffrey

BRICS Report Series RS-94-43 ISSN 0909-0878 December 1994 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1994, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@daimi.aau.dk

A complete axiomatization of timed bisimulation for a class of timed regular behaviours (Revised version)

Luca Aceto^{∗} BRICS^{†} Department of Mathematics and Computer Science Aalborg University Fredrik Bajersvej 7E 9220 Aalborg Ø, Denmark

Alan Jeffrey^{‡} School of Cognitive and Computing Sciences University of Sussex, Brighton BN1 9QH, UK

Abstract

One of the most satisfactory results in process theory is Milner’s axiomatization of strong bisimulation for regular CCS. This result holds for open terms with finite-state recursion. Wang has shown that timed bisimulation can also be axiomatized, but only for closed terms without recursion. In this paper, we provide an axiomatization for timed bisimulation of open terms with finite-state recursion.

Key words and phrases. Complete axiomatizations, ω-complete-ness, equational logic, timed bisimulation equivalence, regular processes, timed CCS.

1 Introduction

Much research in concurrency theory has recently been devoted to the development of extensions of standard process algebras like CCS [16], CSP [11] and ACP [3] with constructs allowing for the modelling of timing aspects in the behaviour of processes. By now, most process algebras have a timed counterpart (see, e.g., [1, 6, 18, 21]), and the development of results and techniques for these languages is becoming comparable with that for the standard process description languages. For example, complete axiomatizations of behavioural congruences for subsets of timed process algebras have been presented in, e.g., [10, 14, 18, 22]—showing that behavioural congruences which deal with timing considerations are as mathematically tractable as the standard untimed ones.

∗On leave from School of Cognitive and Computing Sciences, University of Sussex, Brighton BN1 9QH, UK. Email: luca@iesd.auc.dk.

†Basic Research in Computer Science, Centre of the Danish National Research Foundation.

‡Supported by SERC project GR/H 16537. Additional funding was received from EC BRA 7166 concur2. Email: alanje@cogs.susx.ac.uk.

Two of the most beautiful results in the theory of process algebras are the complete axiomatizations of strong bisimulation equivalence and observational congruence for regular CCS processes provided by Milner in his classic papers [15] and [17], respectively. These results have put the notions of behaviour used in the theory of CCS on an equal footing with the one common in formal language theory, and have contributed to the realization that the notion of process is at least as elegant and mathematically tractable as that of language.

The main purpose of this paper is to show that the techniques developed by Milner in [15, 17] can be adapted to provide a complete axiomatization of the notion of timed bisimulation equivalence, due to Wang Yi [21], over a class of regular timed CCS processes [12, 22]. More precisely, we shall offer a complete axiomatization of timed bisimulation over the language of action guarded regular expressions studied in [12]. This complete axiomatization is obtained by combining an improved version of the laws which were shown in [22] to characterize timed bisimulation over finite trees with standard laws for recursively defined processes, viz, laws to unwind recursive definitions of expressions, and a version of unique fixed-point induction.

The paper is organized as follows. Section 2 is devoted to preliminaries, and background material on timed CCS and timed bisimulation. The axiomatization of timed bisimulation is presented and discussed in Section 3, where its soundness is also proved. The proof of completeness of the axiomatization is given in detail in Section 4, and relies on an adaptation of the techniques used by Milner in [15, 17].

As this is not an introductory paper on timed CCS, we have taken the liberty to refer the reader to the original papers by Wang Yi for motivations and examples. We hope, however, that the paper will still be sufficiently readable for the uninitiated reader.

2 Timed regular behaviours and timed bisimulation

The language for expressions that we shall consider in this paper is a generalization of the regular subcalculus of Wang Yi’s timed CCS [21, 23]. This language has been investigated by Holmer, Larsen and Wang Yi in [12], and we shall mostly follow the notation and definitions given in that reference.

As usual, we shall assume a countably infinite set Δ of action names, ranged over by a and b, and a distinguished action τ ∉ Δ. Let Act = Δ ∪ {τ}, be the set of actions, ranged over by μ and ν.

Following [13], we define a monoid (X, +, 0) to be:

• left-cancellative iff (x + y = x + z) ⇒ (y = z), and

• anti-symmetric iff (x + y = 0) ⇒ (x = y = 0).

Examples of left-cancellative anti-symmetric monoids include:

• The singleton set (1, +, 0).

• The natural numbers (N, +, 0).

• The non-negative rationals (Q^{+}, +, 0).

• The non-negative reals (R^{+}, +, 0).

• The countable ordinals (ω_{1}, +, 0).

We can define a partial order on X as:

x ≤ y iff ∃z . x + z = y

It is simple to verify that ≤ is a partial order if (X, +, 0) is a left-cancellative anti-symmetric monoid. A time domain is a left-cancellative anti-symmetric monoid (Tim, +, 0), ranged over by t, u and v, such that ≤ is a total order. Define:

t ∧ u = the minimum of t and u
t ∨ u = the maximum of t and u

and when t ≥ u:

t − u = the unique v such that u + v = t

Let Tim_{+} = Tim \ {0} be the set of positive delays, ranged over by c, d and e. Let Lab = Act ∪ {ε(c) | c ∈ Tim_{+}} be the set of labels, ranged over by σ. Let Var be a countably infinite set of process variables, ranged over by x, y

and z.

The set of regular process expressions over Act, Tim and Var is given by the following grammar:

E ::= 0 | x | μ.E | ε(t).E | E + E | fix(x = E)

The interested reader is referred to [21, 23] for intuition on the operators used in the above definition.

We shall assume the standard notions of free and bound variables in expressions, with fix(x = ) as the binding construct. The set of free variables in an expression E is denoted by fvE. Throughout this paper we shall restrict ourselves to considering regular process expressions in which recursions are action guarded, a notion that is defined below.

Definition A variable x is action guarded in E iff x ∈ AG(E), defined:

AG(0) = Var
AG(x) = Var \ {x}
AG(μ.E) = Var
AG(ε(t).E) = AG(E)
AG(E + F) = AG(E) ∩ AG(F)
AG(fix(x = E)) = AG(E) ∪ {x}

A regular process expression E is well-formed iff for every subexpression of E of the form fix(x = F), x is action guarded in F.

\overline{0 ⟶^{ε(c)} 0}  \overline{μ.P ⟶^{μ} P}  \overline{a.P ⟶^{ε(c)} a.P}

\overline{ε(c + t).P ⟶^{ε(c)} ε(t).P}  \frac{P ⟶^{ε(c)} P′}{ε(t).P ⟶^{ε(t+c)} P′}  \frac{P ⟶^{μ} P′}{ε(0).P ⟶^{μ} P′}

\frac{P ⟶^{μ} P′}{P + Q ⟶^{μ} P′}  \frac{Q ⟶^{μ} Q′}{P + Q ⟶^{μ} Q′}  \frac{P ⟶^{ε(c)} P′, Q ⟶^{ε(c)} Q′}{P + Q ⟶^{ε(c)} P′ + Q′}

\frac{E\{fix(x = E)/x\} ⟶^{σ} P}{fix(x = E) ⟶^{σ} P}

Figure 1: The operational semantics for TC_{0}

For example, the expression (fix(x = τ.x)) + y is well-formed, while the expression fix(x = ε(c).x) is not. The above definition departs slightly from the one given in [12, Definition 2.1]. In particular, the expression (fix(x = τ.x)) + y would not be well-formed according to the definition of [12] because the free variable y does not occur within a subexpression of the form μ.F.

The set of all well-formed regular process expressions is TC, ranged over by E, F and G. The set of all closed, well-formed regular process expressions is TC_{0}, ranged over by P, Q and R. Elements of this set will often be referred to as processes.

Following Milner [17], we shall identify expressions which differ only by the renaming of bound variables. We shall also write E{F_{1}, …, F_{n}/x_{1}, …, x_{n}} for the result of simultaneously substituting F_{i} for each free occurrence of x_{i} in E, renaming bound variables as necessary.

The operational semantics for TC_{0} is given by the labelled transition system (TC_{0}, Lab, →) in Figure 1. The interested reader is referred to [21, 23] for comments on the rules. Note that, following Wang Yi [21, 23], ε(0) has been excluded from the semantics of processes.

To conclude this introductory section, we shall now define the notion of timed bisimulation equivalence [21].

Definition A relation R over TC_{0} is a timed bisimulation iff P R Q implies, for all σ:

• whenever P ⟶^{σ} P′ then, for some Q′, Q ⟶^{σ} Q′ and P′ R Q′.

• whenever Q ⟶^{σ} Q′ then, for some P′, P ⟶^{σ} P′ and P′ R Q′.

The relation of timed bisimulation equivalence, denoted by ∼, is the largest timed bisimulation.

The interested reader is referred to the aforementioned papers by Wang Yi, and to [12] for intuition and examples of processes that are equivalent or inequivalent with respect to ∼. The definition of ∼ can be extended to expressions in the standard way as follows:

Definition Let E and F be expressions with free variables in x̃ = x_{1}, …, x_{m}. Then E ∼ F iff for all vectors P̃ = P_{1}, …, P_{m}, E{P̃/x̃} ∼ F {P̃/x̃}.

Proposition 1 ([21, Theorem 5.1]) Timed bisimulation equivalence forms a congruence over TC.

In the remainder of this paper, we shall present a complete axiomatization of ∼ over TC.

3 Axiomatization and soundness

In [21] various equational laws were proved to hold for Wang Yi’s timed CCS modulo timed bisimulation equivalence, and in [22] a set of such axioms was shown to be complete over the language of recursion-free TC_{0} processes with delays from the time domain of the positive reals. We shall now present an axiomatization which will be proven complete for ∼ over the whole of TC, i.e., complete for regular process expressions with action guarded recursion. The detailed proof of completeness occupies Section 4 of this paper.

Wang’s axiomatization for recursion-free TC_{0} processes is given by the axiom system F in Figures 2 and 3. Our axiomatization for regular TC process expressions is given by the axiom system E in Figures 2 and 4.

The axioms (S1)–(S4) are the standard laws for a complete axiomatization of strong bisimulation equivalence over finite trees [9]. Together with axioms (R1) and (R2), these form a complete axiomatization of strong bisimulation equivalence for guarded regular CCS terms [15]. (In fact, the axiomatization in [15] can be obtained as a special case of that in Figure 2 by taking the time domain to be the singleton set (1, +, 0).)

The axioms (TD), (TA) and (T0) correspond to the operational properties of time determinacy, time additivity and zero delay. These axioms are present in Wang’s [21, 22] axiomatization. As we shall see in Section 4, the axiom system G given in Figure 2 is powerful enough to prove Milner’s [15] Equational Characterization Theorem for timed regular expressions. However, G is not powerful enough to give a complete axiomatization for recursion-free timed expressions.

Wang [21, 22] added the axioms (MP), (AP) and (NP) to G to provide a complete axiomatization for recursion-free TC_{0} processes. These axioms correspond to the operational properties of maximal progress and persistency, and are discussed in detail by Wang. However, the resulting axiom system F, given in Figure 3, is not powerful enough to give a complete axiomatization for recursion-free TC process expressions.

Our axiomatization replaces (AP) and (NP) with one new persistency axiom (P). In Section 4 we show that E is complete for timed bisimulation equivalence over TC process expressions. In Section 5 we show that E is strictly stronger than F, and thus that Wang’s axiomatization is not complete for open TC process expressions.

(S1)  E + F = F + E
(S2) E + (F + G) = (E + F) + G
(S3)  E + E = E
(S4)  E + 0 = E
(TD) ε(t).(E + F) = ε(t).E + ε(t).F
(TA)  ε(t + u).E = ε(t).ε(u).E
(T0)  ε(0).E = E
(R1) fix(x = E) = E{fix(x = E)/x}
(R2) If F = E{F/x}, then F = fix(x = E), if x is action guarded in E

Figure 2: The axiom system G

\begin{aligned}(MP) & τ.E + ε(c).F & = & τ.E \\ (AP) & a.E + ε(t).a.E & = & a.E \\ (NP) & ε(t).0 & = & 0 \end{aligned}

Figure 3: The axiom system F is G plus (MP), (AP) and (NP)

\begin{aligned}(MP) & τ.E + ε(c).F & = & τ.E \\ (P) & E + ε(t).E & = & E \end{aligned}

Figure 4: The axiom system E is G plus (MP) and (P)

We shall write E ⊢ E = F when E = F may be proved from E together with the structural rules for = to be a congruence, and similarly for F ⊢ E = F and G ⊢ E = F.

To conclude this section, we shall show that E is indeed sound with respect to timed bisimulation equivalence over TC.

Proposition 2 (Soundness) For all TC expressions E, F, E ⊢ E = F implies E ∼ F.

Proof. All the laws in E have been shown sound by Wang Yi in [22]. The only exception is the persistency axiom (P), the soundness of which is established by the timed bisimulation:

∼ ∘ ({(Q + P, Q) | ∃c . P ⟶^{ε(c)} Q} ∪ {(P, P) | P ∈ TC_{0}}) ∘ ∼

where ∘ denotes composition of relations. The proof that this relation is a bisimulation depends on the properties of time determinacy, time additivity and persistency of the operational semantics for TC_{0}, and the soundness of (T0). (The interested reader is referred to [21] and [20] for details on these properties). □

4 Completeness

In this section, we shall present the proof of completeness of the set of laws E over TC. The structure of the proof of this result will follow closely the most beautiful arguments used by Milner in [15, 17] to prove the completeness of the axiomatizations for strong bisimulation and observational congruence over regular CCS processes.

The structure of the completeness proof will be as follows: first of all, we shall show that every TC expression E provably satisfies a certain kind of equation set. This is what Milner calls the Equational Characterization Theorem. Next, we shall show that if E ∼ F and E provably satisfies an equation set, while F provably satisfies another equation set, then both E and F provably satisfy a common equation set. Finally, we show that whenever two TC expressions provably satisfy the same equation set, then E proves that they are equal.

Definition An equation set x̃ = Ẽ is a finite non-empty sequence of declarations x_{1} = E_{1}, …, x_{n} = E_{n}, where the x_{i}s are pairwise distinct variables, and the E_{i}s are TC expressions.

A vector F̃ = F_{1} … F_{n} satisfies x̃ = Ẽ iff ∀i . F_{i} ∼ E_{i}{F̃/x̃}.

For an equational theory T , a vector F̃ = F_{1} … F_{n} T -provably satisfies x̃ = Ẽ iff ∀i . T ⊢ F_{i} = E_{i}{F̃/x̃}.

An expression E (T -provably) satisfies x̃ = F̃ iff we can find a vector Ẽ which (T -provably) satisfies x̃ = F̃ and E ∼ E_{1} (T ⊢ E = E_{1}).

We refer to x_{1} as the leading variable of the equation set x̃ = F̃.

For example, the equation set:

x_{1} = ε(1).a.x_{2} + ε(3).y  x_{2} = ε(2).b.x_{1}  (1)

is satisfied by fix(z = ε(1).a.ε(2).b.z + ε(3).y).

Definition An equation set x̃ = Ẽ is standard iff each E_{i} is of the form:

∑_{j∈J_{i}} ε(t_{j}).μ_{j}.x_{j} + ∑_{k∈K_{i}} ε(u_{k}).w_{k}

where the vectors x̃ and w̃ are disjoint. By convention, we indentify each E_{i} with 0 when the index sets J_{i} and K_{i} are both empty. We call x̃ the formal variables of x̃ = Ẽ, and w̃ the free variables of x̃ = Ẽ.

For example, the above equation set (1) is standard, but the following is not:

x_{1} = ε(1).x_{2} + ε(3).y, x_{2} = a.ε(2).b.x_{1}

Proposition 3 If x̃ = Ẽ is standard and w is not a formal variable, then we can find a standard x̃ = F̃ such that ∀i . G ⊢ F_{i} = E_{i}{E_{1}/w}.

Proof. Define F̃ as:

F_{i} ≡ ∑_{j∈J_{i}} ε(t_{j}).μ_{j}.x_{j} + ∑_{\begin{matrix}k ∈ K_{i} \\ w_{k} ≠ w \end{matrix}}ε(u_{k}).w_{k}

+ ∑_{\begin{matrix}k ∈ K_{i} \\ w_{k} = w \\ j′ ∈ J_{1} \end{matrix}}ε(u_{k} + t_{j′}).μ_{j′}.x_{j′} + ∑_{\begin{matrix}k ∈ K_{i} \\ w_{k} = w \\ k′ ∈ K_{1} \end{matrix}}ε(u_{k} + u_{k′}).w_{k′}

It is simple to show that this is standard, and that ∀i . G ⊢ F_{i} = E_{i}{E_{1}/w}. □

Proposition 4 If x is action guarded in E and G ⊢ E = F then x is action guarded in F.

Proof. Show that AG( ) is a model for the equational theory G. □

Proposition 5 We shall use the following standard results about substitution:

1. G{F̃/x̃}{E/w} ≡ G{E/w}{F̃{E/w}/x̃}, if w does not occur in x̃, and x̃ are not free in E.

2. F {G/w}{Ẽ/x̃} ≡ F {G{Ẽ/x̃}/w}{Ẽ/x̃}, if x̃ are not free in Ẽ.

Proof. Routine structural induction. □

Theorem 6 (Equational Characterization) For any E we can find a standard equation set x̃ = G̃ which E G-provably satisfies. Moreover E and the equation set x̃ = G̃ have the same free variables.

Proof. An induction on E. The only difficult case is when E ≡ fix(w = F). In this case, by induction we find a x̃ = H̃ which F G-provably satisfies, and wlog we can assume that w is not a formal variable of x̃ = H̃, and that x̃ are not free in E. Thus we have a F̃ such that:

G ⊢ F_{1} = F  (2)
∀i . G ⊢ F_{i} = H_{i}{F̃/x̃}  (3)

Define:

E_{i} ≡ F_{i}{E/w}  (4)

Let G̃ be the standard equation set given by Proposition 3 such that:

G ⊢ G_{i} = H_{i}{H_{1}/w}  (5)

Since w is action guarded in F, by Proposition 4 it must be action guarded in H_{1}{F̃/x̃}, so, as w ∉ x̃, must be action guarded in H_{1}, so cannot be free in H_{1}. Then:

G ⊢ E

= F {E/w}  (R1)
= F_{1}{E/w}  (2)
= E_{1}  (4)

and:

G ⊢ E_{1}
= F_{1}{E/w}  (4)
= H_{1}{F̃/x̃}{E/w}  (3)
= H_{1}{E/w}{F̃{E/w}/x̃}  (Propn 5.1)
= H_{1}{E/w}{Ẽ/x̃}  (4)
= H_{1}{Ẽ/x̃}  (w ∉ fvH_{1})

and so:

G ⊢ E_{i}
= F_{i}{E/w}  (4)
= H_{i}{F̃/x̃}{E/w}  (3)
= H_{i}{E/w}{F̃{E/w}/x̃}  (Propn 5.1)
= H_{i}{E/w}{Ẽ/x̃}  (4)
= H_{i}{H_{1}{Ẽ/x̃}/w}{Ẽ/x̃}  (above)
= H_{i}{H_{1}/w}{Ẽ/x̃}  (Propn 5.2)
= G_{i}{Ẽ/x̃}  (5)

Thus we have found a standard x̃ = G̃ which E G-provably satisfies. □

Theorem 6 shows that every expression E in TC G-provably satisfies a standard equation set x̃ = G̃. The second stepping stone towards the promised completeness theorem is a result showing that if E ∼ F, where F G-provably satisfies a standard equation set ỹ = H̃, then there exists a third standard equation set E-provably satisfied by both E and F. Note that this part of the completeness proof requires the axioms (MP) and (P).

Theorem 7 Let E and E′ be expressions in TC such that E ∼ E′. Assume that E E-provably satisfies a standard equation set x̃ = F̃, and E′ E-provably satisfies a standard equation set x̃′ = F̃′. Then there exists a standard equation set E-provably satisfied by both E and E′.

Proof (Following Milner). Assume that:

F_{i} ≡ ∑_{j∈J_{i}} ε(t_{j}).a_{j}.x_{j} + ∑_{k∈K_{i}} ε(u_{k}).τ.x_{k} + ∑_{l∈L_{i}} ε(v_{l}).w_{l}  (6)
F′_{i′} ≡ ∑_{j′∈J′_{i′}} ε(t′_{j′}).a_{j′}.x′_{j′} + ∑_{k′∈K′_{i′}} ε(u′_{k′}).τ.x′_{k′} + ∑_{l′∈L′_{i′}} ε(v′_{l′}).w′_{l′}  (7)

As E E-provably satisfies x̃ = F̃ and E′ E-provably satisfies x̃′ = F̃′, we can find Ẽ and Ẽ′ such that:

E ⊢ E = E_{1}  (8)

∀i . E ⊢ E_{i} = F_{i}{Ẽ/x̃}  (9)
E ⊢ E′ = E′_{1}  (10)
∀i . E ⊢ E′_{i} = F′_{i}{Ẽ′/x̃′}  (11)

Let w̃ denote the set of free variables occurring in either E or E′. Choose a vector ã of distinct actions, one action a_{w} for each w ∈ w̃, that do not occur in E and E′. (This is always possible as the set of action names Δ is countably infinite.) Take the vector P̃ of processes given by P_{w} ≡ a_{w}.0. As E ∼ E′, it follows, in particular, that E{P̃/w̃} ∼ E′{P̃/w̃}. Thus, by (8) and (10), we have that E_{1}{P̃/w̃} ∼ E′_{1}{P̃/w̃}.

Let R be the relation {(i, i′) | E_{i}{P̃/w̃} ∼ E′_{i′}{P̃/w̃}}, let z̃ be the vector of fresh variables {z_{ii′} | i R i′} (with z_{11} as leading variable), and define the vectors G̃, H̃ and H̃′ as:

G_{ii′} ≡ ∑_{\begin{matrix}j ∈ J_{i}, j′ ∈ J′_{i′} \\ j R j′, a_{j} = a′_{j′} \end{matrix}} ε(t_{j} ∨ t′_{j′}).a_{j}.z_{jj′} + ∑_{\begin{matrix}k ∈ K_{i}, k ∈ K′_{i′} \\ k R k′ \end{matrix}} ε(u_{k} ∨ u′_{k′}).τ.z_{kk′} + ∑_{\begin{matrix}l ∈ L_{i}, l′ ∈ L′_{i′} \\ w_{l} = w′_{l′} \end{matrix}} ε(v_{l} ∨ v′_{l′}).w_{l}(12)

H_{ii′} ≡ E_{i}  (13)
H′_{ii′} ≡ E′_{i′}  (14)

Note that the equation set z̃ = G̃ is standard by construction. We now show that the vector H̃ E-provably satisfies z̃ = G̃. To this end, we prove, first of all, that, for each i R i′, every summand of G_{ii′}{H̃/z̃} can be absorbed into H_{ii′}. We consider three cases, depending on the form taken by the summand of G_{ii′}{H̃/z̃}.

For any i R i′, j ∈ J_{i} and j′ ∈ J′_{i′} such that j R j′ and a_{j} = a′_{j′}:

E ⊢ H_{ii′}

= E_{i}  (13)
= F_{i}{Ẽ/x̃}  (9)
= F_{i}{Ẽ/x̃} + ε(t_{j}).a_{j}.E_{j}  (S1–S3,6)
= F_{i}{Ẽ/x̃} + ε(t_{j}).(a_{j}.E_{j} + ε((t_{j} ∨ t′_{j′}) − t_{j}).a_{j}.E_{j})  (P)
= F_{i}{Ẽ/x̃} + ε(t_{j}).a_{j}.E_{j} + ε(t_{j}).ε((t_{j} ∨ t′_{j′}) − t_{j}).a_{j}.E_{j}  (TD)
= F_{i}{Ẽ/x̃} + ε(t_{j}).a_{j}.E_{j} + ε(t_{j} + ((t_{j} ∨ t′_{j′}) − t_{j})).a_{j}.E_{j}  (TA)
= F_{i}{Ẽ/x̃} + ε(t_{j}).a_{j}.E_{j} + ε(t_{j} ∨ t′_{j′}).a_{j}.E_{j}  (t + (u − t) = u)
= F_{i}{Ẽ/x̃} + ε(t_{j} ∨ t′_{j′}).a_{j}.E_{j}  (S1–S3,6)
= E_{i} + ε(t_{j} ∨ t′_{j′}).a_{j}.E_{j}  (9)
= H_{ii′} + ε(t_{j} ∨ t′_{j′}).a_{j}.H_{jj′}  (13)
= H_{ii′} + ε(t_{j} ∨ t′_{j′}).a_{j}.z_{jj′}{H̃/z̃}  (substitution)

Similarly, for any i R i′, k ∈ K_{i} and k′ ∈ K′_{i′} such that k R k′:

E ⊢ H_{ii′} = H_{ii′} + ε(u_{k} ∨ u′_{k′}).τ.z_{kk′}{H̃/z̃}

and for any i R i′, l ∈ L_{i} and l′ ∈ L′_{i′} such that w_{l} = w′_{l′}:

E ⊢ H_{ii′} = H_{ii′} + ε(v_{l} ∨ v′_{l′}).w_{l}{H̃/z̃}

We remark here that the proof of the above equality makes an essential use of axiom (P), and could not have been carried out using Wang’s persistency axioms (AP) and (NP).

Thus each summand of G_{ii′}{H̃/z̃} can be absorbed into H_{ii′}, and by (S1)– (S4):

E ⊢ H_{ii′} = H_{ii′} + G_{ii′}{H̃/z̃}  (15)

We now show that the converse also holds, namely that H_{ii′} can be absorbed into G_{ii′}{H̃/z̃}. To this end, by (9) and (13), it is sufficient to prove that each summand of F_{i}{Ẽ/x̃} can be absorbed into G_{ii′}{H̃/z̃}. Again, we distinguish three cases depending on the form the summand takes.

For any i R i′ and j ∈ J_{i}, either:

• t_{j} ≤ u_{k}, for every k ∈ K_{i}, or:

• there exists k ∈ K_{i} such that t_{j} > u_{k}.

We proceed to show that in either case:

E ⊢ G_{ii′}{H̃/z̃} = G_{ii′}{H̃/z̃} + ε(t_{j}).a_{j}.x_{j}{Ẽ/x̃}

• Case ∀k ∈ K_{i} . t_{j} ≤ u_{k}. In this case, by the operational semantics for TC_{0}, it follows that:

F_{i}{Ẽ/x̃}{P̃/w̃} ⟶^{ε(t_{j})}⟶^{a_{j}} E_{j}{P̃/w̃}

As E_{i}{P̃/w̃} ∼ E′_{i′}{P̃/w̃} and G is sound for ∼, we have that

F_{i}{Ẽ/x̃}{P̃/w̃} ∼ F′_{i′}{Ẽ/x̃′}{P̃/w̃}

So, as the actions in ã were chosen to be fresh:

F′_{i′}{Ẽ′/x̃′}{P̃/w̃} ⟶^{ε(t_{j})}⟶^{a_{j}} E′_{j′}{P̃/w̃}

for some j′ with t_{j} ≥ t′_{j′}, a_{j} = a′_{j′} and E_{j}{P̃/w̃} ∼ E′_{j′}{P̃/w̃}. By the definition of the relation R, it follows that j R j′. Thus:

E ⊢ G_{ii′}{H̃/z̃}
= G_{ii′}{H̃/z̃} + ε(t_{j} ∨ t′_{j′}).a_{j}.H_{jj′}  (S1–S3,12)
= G_{ii′}{H̃/z̃} + ε(t_{j}).a_{j}.H_{jj′}  (t_{j} ≥ t′_{j′})
= G_{ii′}{H̃/z̃} + ε(t_{j}).a_{j}.E_{j}  (13)
= G_{ii′}{H̃/z̃} + ε(t_{j}).a_{j}.x_{j}{Ẽ/x̃}  (substitution)

• Case ∃k ∈ K_{i} . t_{j} > u_{k}. Choose k such that u_{k} is minimal in the set {u_{h} | h ∈ K_{i}}. Then, by the operational semantics for TC_{0}:

F_{i}{Ẽ/x̃}{P̃/w̃} ⟶^{ε(u_{k})}⟶^{τ} E_{k}{P̃/w̃}

Therefore, as in the previous case, we have:

F′_{i′}{Ẽ′/x̃′}{P̃/w̃} ⟶^{ε(u_{k})}⟶^{τ} E′_{k′}{P̃/w̃}

for some k′ ∈ K′_{i′} with u_{k} ≥ u′_{k′} and k R k′. In fact, by symmetry and the fact that u_{k} is minimal in the set {u_{h} | h ∈ K_{i}}, it is easy to see that u_{k} = u′_{k′}. Thus:

E ⊢ G_{ii′}{H̃/z̃}

= G_{ii′}{H̃/z̃} + ε(u_{k} ∨ u′_{k′}).τ.H_{kk′}  (S1–S3,12)
= G_{ii′}{H̃/z̃} + ε(u_{k}).τ.H_{kk′}  (u_{k} = u′_{k′})
= G_{ii′}{H̃/z̃} + ε(u_{k}).(τ.H_{kk′} + ε(t_{j} − u_{k}).a_{j}.H_{jj′}) (MP,t_{j} > u_{k})
= G_{ii′}{H̃/z̃} + ε(u_{k}).τ.H_{kk′} + ε(u_{k}).ε(t_{j} − u_{k}).a_{j}.H_{jj′}  (TD)
= G_{ii′}{H̃/z̃} + ε(u_{k}).τ.H_{kk′} + ε(u_{k} + (t_{j} − u_{k})).a_{j}.H_{jj′}  (TA)
= G_{ii′}{H̃/z̃} + ε(u_{k}).τ.H_{kk′} + ε(t_{j}).a_{j}.H_{jj′}  (t + (u − t) = u)
= G_{ii′}{H̃/z̃} + ε(u_{k} ∨ u′_{k′}).τ.H_{kk′} + ε(t_{j}).a_{j}.H_{jj′}  (u_{k} = u′_{k′})
= G_{ii′}{H̃/z̃} + ε(t_{j}).a_{j}.H_{jj′}  (S1–S3,12)
= G_{ii′}{H̃/z̃} + ε(t_{j}).a_{j}.E_{j}  (13)
= G_{ii′}{H̃/z̃} + ε(t_{j}).a_{j}.x_{j}{Ẽ/x̃}  (substitution)

Note that the above reasoning uses the equation (MP).

Thus:

E ⊢ G_{ii′}{H̃/z̃} = G_{ii′}{H̃/z̃} + ε(t_{j}).a_{j}.x_{j}{Ẽ/x̃}

Similarly, for any i R i′ and k ∈ K_{i}, it is not too difficult to prove that:

E ⊢ G_{ii′}{H̃/z̃} = G_{ii′}{H̃/z̃} + ε(u_{k}).τ.x_{k}{Ẽ/x̃}

We are now left to show that for any i R i′ and l ∈ L_{i}:

E ⊢ G_{ii′}{H̃/z̃} = G_{ii′}{H̃/z̃} + ε(v_{l}).w_{l}{Ẽ/x̃}  (16)

As before, we prove this statement by considering the following two sub-cases:

• v_{l} ≤ u_{k}, for every k ∈ K_{i}, or:

• there exists k ∈ K_{i} such that v_{l} > u_{k}.

The proof of (16) when there exists k ∈ K_{i} such that v_{l} > u_{k} follows the lines spelled out in detail above. We shall thus concentrate on presenting a detailed proof of (16) in the case v_{l} ≤ u_{k}, for every k ∈ K_{i}.

Assume that l ∈ L_{i} and that v_{l} ≤ u_{k}, for every k ∈ K_{i}. We claim that there exists l′ ∈ L′_{i′} such that v′_{l′} ≤ v_{l} and w_{l} = w′_{l′}. To see that this is indeed the case, note that, by (9), (11) and the soundness of E:

F_{i}{Ẽ/x̃}{P̃/w̃} ∼ F′_{i′}{Ẽ′/x̃′}{P̃/w̃}  (17)

As l ∈ L_{i} and v_{l} ≤ u_{k}, for every k ∈ K_{i}, it follows that F_{i}{Ẽ/x̃}{P̃/w̃} ⟶^{ε(v_{l})}⟶^{a_{w_{l}}}.

By (17) and the fact that a_{w_{l}} does not occur in F′_{i′}{Ẽ′/x̃′}, we then have that

F′_{i′}{Ẽ′/x̃′}{P̃/w̃} ⟶^{ε(v_{l})}⟶^{a_{w_{l}}} hence, for some l′ ∈ L′_{i′}, we have v′_{l′} ≤ v_{l} and

w′_{l′} = w_{l} as claimed.

Now we can easily prove (16) as follows:

E ⊢ G_{ii′}{H̃/z̃}
= G_{ii′}{H̃/z̃} + ε(v_{l} ∨ v′_{l′}).w_{l}  (S1–S3,12)
= G_{ii′}{H̃/z̃} + ε(v_{l}).w_{l}  (v′_{l′} ≤ v_{l})
= G_{ii′}{H̃/z̃} + ε(v_{l}).w_{l}{Ẽ/x̃}  (substitution)

Thus each summand of F_{i}{Ẽ/x̃} can be absorbed into G_{ii′}{H̃/z̃}, and by (S1)– (S4):

E ⊢ G_{ii′}{H̃/z̃} = G_{ii′}{H̃/z̃} + F_{i}{Ẽ/x̃}  (18)

Hence:

E ⊢ H_{ii′}
= H_{ii′} + G_{ii′}{H̃/z̃}  (15)
= E_{i} + G_{ii′}{H̃/z̃}  (13)
= F_{i}{Ẽ/x̃} + G_{ii′}{H̃/z̃}  (9)
= G_{ii′}{H̃/z̃}  (18)

Thus H̃ E-provably satisfies z̃ = G̃, and E ⊢ E = E_{1} = H_{11} so E E-provably satisfies z̃ = G̃. Similarly, E′ E-provably satisfies z̃ = G̃. □

The final ingredient of the proof of completeness is a result showing that every standard equation set has a unique solution up to provable equality.

Theorem 8 (Unique Solution) If x̃ = H̃ is a standard equation set, then there is a TC expression E which E-provably satisfies it. Moreover, if another TC expression F also E-provably satisfies x̃ = H̃, then E ⊢ E = F.

Proof. The claim follows from the following, slightly stronger statement:

Let x̃ = x_{1}, …, x_{m} and w̃ = w_{1}, …, w_{n} be disjoint vectors of pairwise distinct variables, and H̃ = {H_{1}, …, H_{m}} be well-formed expressions with free variables in x̃ ∪ w̃ in which each variable x_{i} is action guarded. Consider the equation set x̃ = H̃. Then there exists an expression E ∈ TC which E-provably satisfies it. Moreover, if F also E-provably satisfies x̃ = H̃, then E ⊢ E = F.

This is proven by induction on m by a simple reworking of the proof of Theorem 5.7 in [15]. The interested reader will have no difficulty in filling in the details following Milner’s proof. □

We are now in a position to prove the completeness of E.

Theorem 9 (Completeness) For all TC expressions E, F, E ∼ F implies E ⊢ E = F.

Proof. By Theorem 6, E may be proved to satisfy a standard equation set; likewise F. By Theorem 7, E and F may be proved to satisfy a single standard equation set. Finally, Theorem 8 ensures that E ⊢ E = F. □

The following theorem is an interesting corollary of our previous results. We report it here because it gives a simple way of establishing timed bisimilarity between TC expressions which could be easily implemented in an automatic verification tool like, e.g., Epsilon [5].

Theorem 10 Let E, F be TC expressions with free variables in w̃. Let ã be a vector of distinct actions not occurring in E and F, one such action for each w ∈ w̃. Take P_{w} ≡ a_{w}.0. Then E{P̃/w̃} ∼ F {P̃/w̃} implies E ∼ F.

Proof. Suppose that E{P̃/w̃} ∼ F {P̃/w̃}, where {P̃/w̃} is a substitution meeting the proviso of the theorem. An inspection of the proof of Theorem 8 then shows that E and F E-provably satisfy a common standard equation set. By Theorem 7, we then have that E ⊢ E = F. The claim now follows by the soundness of E with respect to ∼. □

5 Comparison with Wang’s axiomatization

In this section we show that the theory E is strictly stronger than Wang’s F over TC. More precisely, we shall prove that if F proves an equality E = F, then so does E. On the other hand, F is not strong enough to prove the new persistency axiom (P).

Proposition 11 For all E, F ∈ TC, F ⊢ E = F implies E ⊢ E = F.

Proof. A straightforward induction on the length of the proof of the equation E = F from the theory F. Note that axiom (AP) is an instance of axiom (P), and that an application of axiom (NP) can be mimicked using (P) and (S1)–(S4). □

Proposition 12 F ⊬ E = E + ε(t).E

Proof. Define a denotational semantics for TC in the domain {0, 1, 2} with the semantics:

[[x]]ρ = ρ(x)
[[0]]ρ = 0
[[μ.E]]ρ = 2
[[ε(0).E]]ρ = [[E]]ρ
[[ε(c).E]]ρ = \{ \begin{matrix}0 & if [[E]]ρ = 0 \\ 2 & otherwise \end{matrix}
[[E + F]]ρ = max([[E]]ρ, [[F]]ρ)
[[fix(x = E)]]ρ = the least fixed point of the function λd. [[E]]ρ[x ↦ d]

where ρ : Var → {0, 1, 2}, and ρ[x ↦ d] stands for the function that maps x to d and agrees with ρ on all the other variables.

Note that, because of our requirement that expressions be well-formed, the function λd. [[E]]ρ[x ↦ d] used in the definition of the semantics of recursive expressions has always a unique fixed point. It is now simple to check that this is a model for F, but

[[x + ε(c).x]](λx.1) = 2 ≠ 1 = [[x]](λx.1)

and so it is not a model for E. □

However, all the closed instantiations of (P) can be derived from F, as the following proposition shows.

Proposition 13 For every P ∈ TC_{0}, F ⊢ P = P + ε(t).P.

Proof. By Theorem 6, for some finite index set I, actions μ_{i} ∈ Act, delays t_{i} ∈ Tim and processes P_{i} ∈ TC_{0}:

G ⊢ P = ∑_{i∈I} ε(t_{i}).μ_{i}.P_{i}  (19)

Now:

F ⊢ P

= ∑_{i∈I} ε(t_{i}).μ_{i}.P_{i}  (19)
= ∑_{i∈I} ε(t_{i}).(μ_{i}.P_{i} + ε((t + t_{i}) − t_{i}).μ_{i}.P_{i})  (AP, or MP if μ_{i} = τ)
= ∑_{i∈I} ε(t_{i}).μ_{i}.P_{i} + ε(t_{i}).ε((t + t_{i}) − t_{i}).μ_{i}.P_{i}  (TD)
= ∑_{i∈I} ε(t_{i}).μ_{i}.P_{i} + ε(t_{i} + ((t + t_{i}) − t_{i})).μ_{i}.P_{i}  (TA)
= ∑_{i∈I} ε(t_{i}).μ_{i}.P_{i} + ε(t + t_{i}).μ_{i}.P_{i}  (t + (u − t) = u)
= ∑_{i∈I} ε(t_{i}).μ_{i}.P_{i} + ε(t).ε(t_{i}).μ_{i}.P_{i}  (TA)
= ∑_{i∈I} ε(t_{i}).μ_{i}.P_{i} + ∑_{i∈I} ε(t).ε(t_{i}).μ_{i}.P_{i}  (S1,S2)
= ∑_{i∈I} ε(t_{i}).μ_{i}.P_{i} + ε(t). ∑_{i∈I} ε(t_{i}).μ_{i}.P_{i}  (TD,NP)
= P + ε(t).P  (19)

Thus F can show any closed instantiation of axiom (P). □

Note that throughout the above proof we have been careful not to assume that the monoidal operation + on the time domain is commutative. Although this is true for most of the examples of time domain one encounters in the literature, it does not hold for, e.g., the time domain of the countable ordinals (ω_{1}, +, 0).

6 Concluding remarks

In this paper, we have presented a complete axiomatization of timed bisimulation equivalence over open terms with finite-state recursion in a generalization of the regular subcalculus of Wang’s timed CCS. Our inference system for timed bisimulation equivalence is obtained by combining an improved version of Wang’s complete axiomatization for finite trees [22] with standard laws for recursively defined processes. The proof of completeness of the proposed axiomatization uses an adaptation of Milner’s classic arguments presented in [15, 17].

The axiomatization we have presented is parametric with respect to the chosen time domain, and will hold for many of the models of time that have been considered in the literature on timed process algebras, e.g., the natural numbers, the non-negative rationals and the non-negative reals. The definition of time domain that we have chosen in this paper is due to Jeffrey, Schneider and Vaandrager [13] and suits the purpose of this paper well. However, it is certainly not the only one possible, and several ones have been proposed in the literature (see [4] for a series of examples).

Complete axiomatizations of behavioural equivalences for several timed process algebras have been presented in the literature; see, e.g., [7, 10, 14, 18, 19, 22] for examples of such results. With the notable exception of the one presented in [10], all the aforementioned axiomatizations are restricted to recursion-free processes. Hennessy and Regan’s axiomatization of their behavioural precongruence over the language TPL includes an infinitary conditional equation, the so-called ω-induction rule, whose validity is justified by the algebraicity [8] of their testing-based semantics. To the best of our knowledge, the work reported in this paper is the first to offer a finitary complete axiomatization for a class of timed behaviours with finite-state recursion.

The axiomatization of strong bisimulation equivalence presented by Milner in [15] is complete for arbitrary regular CCS expressions. Milner’s inference system deals with unguarded recursive expressions by means of the law:

fix(x = E + x) = fix(x = E)  (20)

Such a law, however, is not sound with respect to timed bisimulation. For example, fix(x = a.0 + x) is not timed bisimulation equivalent to fix(x = a.0), as the latter can delay whereas the former cannot. We conjecture that our complete axiomatization of timed bisimulation can be extended to arbitrary timed regular expressions by extending the language TC with a new constant ℧ denoting the time stop, i.e., a process that cannot perform any action, and, unlike 0, is not allowed to delay. Using ℧, we could then write a version of law (20) as follows:

fix(x = E + x) = fix(x = E + ℧)

The time stop process could then be axiomatized by means of the laws:

℧ + ε(c).E = ℧
℧ + τ.E = τ.E

It is interesting to note that axiom (MP) is derivable from these two laws for ℧.

References

[1] J.C.M. Baeten and J.A. Bergstra. Real time process algebra. Journal of Formal Aspects of Computing Science, 3(2):142–188, 1991.

[2] J.C.M. Baeten and J.W. Klop, editors. Proceedings CONCUR 90, Amsterdam, volume 458 of Lecture Notes in Computer Science. Springer-Verlag, 1990.

[3] J.C.M. Baeten and W.P. Weijland. Process Algebra. Cambridge Tracts in Theoretical Computer Science 18. Cambridge University Press, 1990.

[4] J. van Benthem. Time, logic and computation. In J.W. de Bakker, W.- P. de Roever, and G. Rozenberg, editors, REX School/Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, Noordwijkerhout, volume 354 of Lecture Notes in Computer Science, pages 1–49. Springer-Verlag, 1989.

[5] K. Cerans, J.C. Godskesen, and K.G. Larsen. Timed modal specification — theory and tools. In C. Courcoubetis, editor, Proceedings of the Fifth International Conference Computer Aided Verification, Elounda, Greece, July 1993, volume 697 of Lecture Notes in Computer Science, pages 253– 267. Springer-Verlag, 1993.

[6] J. Davies and S. Schneider. An introduction to Timed CSP. Technical Monograph PRG-75, Oxford University Computing Laboratory, Programming Research Group, August 1989.

[7] J.F. Groote. Specification and verification of real time systems in ACP. Report CS-R9015, CWI, Amsterdam, 1990. An extended abstract appeared in L. Logrippo, R.L. Probert and H. Ural, editors, Proceedings 10^{th} International Symposium on Protocol Specification, Testing and Verification, Ottawa, pages 261–274, 1990.

[8] M. Hennessy. Algebraic Theory of Processes. MIT Press, Cambridge, Massachusetts, 1988.

[9] M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137–161, 1985.

[10] M. Hennessy and T. Regan. A process algebra for timed systems. Report 5/91, Computer Science Department, University of Sussex, 1992. To appear in Information and Computation.

[11] C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall International, Englewood Cliffs, 1985.

[12] U. Holmer, K.G. Larsen, and Wang Yi. Deciding properties of regular real timed processes. Report 91–20, Institut for Electronic Systems, Department of Mathematics and Computer Science, Aalborg University Centre, 1991. An extended abstract appeared in the Proceedings of CAV ’91.

[13] A.S.A. Jeffrey, S. Schneider, and F.W. Vaandrager. A comparison of additivity axioms in timed transition systems. Report CS-R9366, CWI, Amsterdam, 1993. Also available as Computer Science Report 11/93, University of Sussex.

[14] A.S. Klusener. Completeness in real time process algebra. In J.C.M. Baeten and J.F. Groote, editors, Proceedings CONCUR 91, Amsterdam, volume 527 of Lecture Notes in Computer Science, pages 376–392. Springer-Verlag, 1991.

[15] R. Milner. A complete inference system for a class of regular behaviours. Journal of Computer and System Sciences, 28:439–466, 1984.

[16] R. Milner. Communication and Concurrency. Prentice-Hall International, Englewood Cliffs, 1989.

[17] R. Milner. A complete axiomatisation for observational congruence of finite-state behaviors. Information and Computation, 81(2):227–247, May 1989.

[18] F. Moller and C. Tofts. A temporal calculus of communicating systems. In Baeten and Klop [2], pages 401–415.

[19] X. Nicollin and J. Sifakis. The algebra of timed processes ATP: Theory and application (revised version). Technical Report RT-C26, LGI-IMAG, Grenoble, France, November 1991.

[20] X. Nicollin and J. Sifakis. An overview and synthesis on timed process algebras. In K.G. Larsen and A. Skou, editors, Proceedings of the Third Workshop on Computer Aided Verification, Aalborg, Denmark, July 1991, volume 575 of Lecture Notes in Computer Science, pages 376–398. Springer-Verlag, 1992.

[21] Wang Yi. Real-time behaviour of asynchronous agents. In Baeten and Klop [2], pages 502–520.

[22] Wang Yi. A calculus of real time systems. PhD thesis, Chalmers University of Technology, Göteborg, Sweden, 1991.

[23] Wang Yi. CCS + time = an interleaving model for real time systems. In J. Leach Albert, B. Monien, and M. Rodríguez, editors, Proceedings 18^{th} ICALP, Madrid, volume 510 of Lecture Notes in Computer Science. Springer-Verlag, 1991.

Recent Publications in the BRICS Report Series

RS-94-43 Luca Aceto and Alan Jeffrey. A Complete Axiomatization of Timed Bisimulation for a Class of Timed Regular Behaviours (Revised Version). December 1994. 18 pp. To appear in Theoretical Computer Science.

RS-94-42 Dany Breslauer and Leszek Ga�sieniec. Ef�cient String Matching on Coded Texts. December 1994. 20 pp.

RS-94-41 Peter Bro Miltersen, Noam Nisan, Shmuel Safra, and Avi Wigderson. On Data Structures and Asymmetric Communication Complexity. December 1994. 17 pp.

RS-94-40 Luca Aceto and Anna Ing� olfsd� ottir. CPO Models for GSOS Languages � Part I: Compact GSOS Languages. December 1994. 70 pp. An extended abstract of the paper will appear in: Proceedings of CAAP ’95, LNCS, 1995.

RS-94-39 Ivan Damg� ard, Oded Goldreich, and Avi Wigderson. Hashing Functions can Simplify Zero-Knowledge Protocol Design (too). November 1994. 18 pp.

RS-94-38 Ivan B. Damg� ard and Lars Ramkilde Knudsen. Enhancing the Strength of Conventional Cryptosystems. November 1994. 12 pp.

RS-94-37 Jaap van Oosten. Fibrations and Calculi of Fractions. November 1994. 21 pp.

RS-94-36 Alexander A. Razborov. On provably disjoint NP-pairs. November 1994. 27 pp.

RS-94-35 Gerth St�lting Brodal. Partially Persistent Data Structures of Bounded Degree with Constant Update Time. November 1994. 24 pp.

RS-94-34 Henrik Reif Andersen, Colin Stirling, and Glynn Winskel. A Compositional Proof System for the Modal μ-Calculus. October 1994. 18 pp. Appears in: Proceedings of LICS ’94, IEEE Computer Society Press.

RS-94-33 Vladimiro Sassone. Strong Concatenable Processes: An Approach to the Category of Petri Net Computations. October 1994. 40 pp.