Timed Processes: Models, Axioms and Decidability

Liang Chen

Doctor of Philosophy

University of Edinburgh

Abstract

This thesis presents and studies a timed computational model of parallelism, a Timed Calculus of Communicating Systems or Timed CCS for short. Timed CCS is an extension of Milner’s CCS with time. We allow time to be discrete, such as the natural numbers, or dense, such as the non-negative rationals or the nonnegative reals. We make no assumption of the Maximal Progress Principle, but the calculus is consistent with the principle. Time variables in the language allow us to express a notion of time dependency and the language is more expressive than those without time variables or infinite summation. We extend the well known notion of bisimulation to timed processes and study the abstract semantics of timed processes. We show that strong equivalence (the largest strong bisimulation) is decidable for finite processes, i.e. processes without recursion. The decidability is independent of the choice of time domain. We also present a simple proof system for strong equivalence and the proof system is again independent of the choice of time domain. We show that the proof system is sound and complete for finite processes over dense time domains, but only complete for a restricted language over discrete time domains. We discuss how to modify the definition of time expressions to get the restricted language. We also study behavioural abstraction in timed processes.

The thesis also presents and studies a general model, Timed Synchronisation Trees, for timed calculi. Timed synchronisation trees are extensions of synchronisation trees with time. All constructions on timed synchronisation trees are continuous with respect to a natural complete partial order. We can interpret a wide range of real-time process algebras in timed synchronisation trees. As an example, we give a denotational semantics for Timed CCS based on timed synchronisation trees. We show that the denotational and operational semantics of Timed CCS coincide.

CCS is a symbolic calculus in the sense that it treats solely the observation of events of a system. The relative time, location and duration of events are abstracted away from the consideration. If we postulate that every action has a non-zero constant duration, we can observe the usual notions of causality, concurrency and conflict relations of events of a system. By interpreting CCS in Timed CCS based on a postulation that for any two events which are causally related there is at least a non-zero constant delay between them, we get a timed semantics for CCS. The timed semantics of CCS is a partial order or true concurrency semantics. As a consequence, we develop a partial order or true concurrency semantics based on an interleaving approach.

Acknowledgement

I would like first of all to thank my first supervisor Stuart Anderson and second supervisor John Power for their help and many invaluable discussions that greatly influenced my work. From them I have learned a lot about research methodology. If I had followed their advice, the contents and presentation of the thesis would be much better.

I also owe a great debt to Faron Moller for his insights, for many fruitful discussions, helpful comments and suggestions, and for reading a draft of this thesis while he was visiting Japan.

I would also like to thank Jos Baeten, Jan Friso Groote, Mark Jerrum, Kim Larsen, Robin Milner, Alistair Munro, Peter Sewell, Colin Stirling and Chris Tofts for their helpful discussions and comments, especially to Robin Milner for his suggestion on studying the models of timed calculi in my thesis proposal committee. Thanks also go to the people in concurrency club for their patience in listening even my half baked ideas and their useful comments.

I want to thank to the staff, students and friends in Edinburgh who enabled me stay and work in such a good environment. Thanks especially go to Davide Sangiorgi for organizing football matches for us and to Soren Christensen for playing badminton.

My thanks to my wife Hong is impossible to be enough in any sense.

My stay in Edinburgh was supported by a TC scholarship of British Council.

Declaration

I hereby declare that this thesis has been composed by myself, the idea, the work and result which I do not attribute to others are due to myself.

Chapter 8 is joint work with Stuart Anderson and Faron Moller [ACM92].

This is the revised version of my thesis incorporating the required corrections suggested by my examiners Kim Larsen and Faron Moller.

Table of Contents

1. Introduction 1

1.1 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.1.1 CCS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.1.2 Hennessy-Milner Logic . . . . . . . . . . . . . . . . . . . . . 10 1.1.3 Labelled Event Structures . . . . . . . . . . . . . . . . . . . 11

1.2 Layout of the Thesis . . . . . . . . . . . . . . . . . . . . . . . . . . 13

2. Timed Synchronisation Trees 16

2.1 A Description of the Model . . . . . . . . . . . . . . . . . . . . . . 17 2.1.1 Timed Synchronisation Trees . . . . . . . . . . . . . . . . . 17 2.1.2 A Complete Partial Order over Ts . . . . . . . . . . . . . . 23

2.2 Constructions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 2.2.1 Empty Constant . . . . . . . . . . . . . . . . . . . . . . . . 26 2.2.2 Prefix . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 2.2.3 Summation . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 2.2.4 Restriction . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 2.2.5 Parallel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Table of Contents vi

2.2.6 Relabelling . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 2.3 An Equivalence over Ts . . . . . . . . . . . . . . . . . . . . . . . . 38 2.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42

3. Timed CCS: A Timed Calculus of Communicating Systems 43 3.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 3.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47

3.2.1 Operational Semantics . . . . . . . . . . . . . . . . . . . . . 47 3.2.2 Denotational Semantics . . . . . . . . . . . . . . . . . . . . 52

3.3 Applications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 3.3.1 Derived Operators . . . . . . . . . . . . . . . . . . . . . . . 54 3.3.2 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58

3.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62

4. Strong Equivalence 65 4.1 Strong Bisimulation . . . . . . . . . . . . . . . . . . . . . . . . . . 65 4.2 Operational Characterization of ≃ . . . . . . . . . . . . . . . . . . 69 4.3 Properties of Strong Equivalence . . . . . . . . . . . . . . . . . . . 71 4.4 Strong Congruence . . . . . . . . . . . . . . . . . . . . . . . . . . . 75 4.5 Unique Solution of Equations . . . . . . . . . . . . . . . . . . . . . 76 4.6 Modal Characterization of ∼ . . . . . . . . . . . . . . . . . . . . . 77

5. Decidability 83 5.1 Characteristic Formulas . . . . . . . . . . . . . . . . . . . . . . . . 84 Table of Contents vii

5.2 Decidability over Discrete Time Domains . . . . . . . . . . . . . . 88 5.3 Decidability over Dense Time Domains . . . . . . . . . . . . . . . . 90

6. A Proof System 91 6.1 The Proof System . . . . . . . . . . . . . . . . . . . . . . . . . . . 92 6.2 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 6.3 Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98

6.3.1 Completeness in Dense Time Domains . . . . . . . . . . . . 99 6.3.2 Completeness in Discrete Time Domains . . . . . . . . . . . 104

6.4 Proofs of Recursively Defined Processes . . . . . . . . . . . . . . . 108 6.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110

7. Behavioural Abstraction in Timed Processes 111 7.1 Weak Bisimulation . . . . . . . . . . . . . . . . . . . . . . . . . . . 111 7.2 Observational Congruence . . . . . . . . . . . . . . . . . . . . . . . 117 7.3 Unique Solution of Equations . . . . . . . . . . . . . . . . . . . . . 125 7.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127

8. Observing Causality in Real-Timed Calculi 128 8.1 An Event Structure Semantics for CCS . . . . . . . . . . . . . . . . 129 8.2 A Timed Semantics for CCS . . . . . . . . . . . . . . . . . . . . . . 132 8.3 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 135

9. Conclusions and Future Work 137

Chapter 1

Introduction

There are two main approaches to the semantics of concurrency, namely the interleaving approach (among others [Mil80,Mil89a,Hoa85,BK84,Hen88a]) and the partial order or true concurrency approach (as in [Rei85,NPW81,BC89,DDM89, Win87]).

Among the interleaving models, Milner’s CCS [Mil80,Mil89a] can be considered to be a standard representative. In [Mil80,Mil89a] Milner has developed a semantic theory of processes based on a notion of bisimulation equivalence. Bisimulation semantics is an elegant mathematical theory of processes. It provides simple and elegant proof techniques for showing that a process implementation meets its specification. However, in this framework, some researchers claim concurrency is not handled in a natural way. The parallelism among actions is described by saying that they can happen in any order. As a consequence, concurrency is reduced to nondeterminism and every concurrent process is equivalent to a nondeterministic sequential process. For any single observation of the behaviour of the system the actions are seen to occur in sequence even though some actions are not causally related. In general, the causality relation and concurrency relation are not observable in interleaving models. For example, in CCS, the process a | b is equivalent to the process ab + ba. In SCCS [Mil83], multisets of actions are allowed thereby providing us a direct representation of “parallelism”. As a result, the process \underline{a} | \underline{b}, where we write \underline{a} in place of δa of SCCS, can be distinguished from the process \underline{a} \underline{b} + \underline{b} \underline{a}. However, causal dependencies are still not recoverable. As an example, process \underline{a} | \underline{b} + \underline{a} \underline{b} cannot be differentiated from process \underline{a} | \underline{b} in SCCS.

The partial order or true concurrency approach provides a more faithful account of the causality, concurrency and conflict or incompatibility relations between events (actions together with their locations) of a system. It describes concurrent computations by means of partial orders. Concurrency between events is represented by the absence of orderings. This approach deals with properties related to knowledge of concurrent activities such as deadlock, fairness, starvation, etc. However, techniques for defining and handling partial orderings are rather weak and there are no corresponding standard mathematical constructions. Among partial order or true concurrency models, Petri Nets [Rei85] and Event Structures [NPW81,Win87] can be considered to be representative.

The traditional methods for reasoning about nondeterministic or concurrent systems, such as [Mil89a,Hoa85,NPW81,Rei85], do not consider hard time aspects of systems. Instead they deal with the quantitative aspects of time in a qualitative way and abstract away explicit time information. There are many systems and applications for which purely qualitative specification and analysis are inadequate. Typical examples are real-time systems, in which the interaction with the environment must satisfy some time constraints. What is important in designing and analysing real-time systems are the significant events and their relative time information.

Real-time systems include fault-tolerant systems, such as protocols, and safety critical systems, such as flight control and radiation control systems. In these systems, it is not sufficient to only say events occur or eventually occur. There are lower and upper bounds on when events can occur relative to the other events. For example, consider an implementation of Alternating Bit Protocol which is based on unreliable transition lines. The transition lines may lose messages. After sending a message to the receiving part via a transition line, the sending part must wait for a certain time, e.g. time Δ, which is the time out of waiting for an acknowledgement before assuming the message has been lost from the transition line. If the sending part receives a correct acknowledgement within time Δ, then it becomes ready to transmit another message. Otherwise, it retransmits the message after a delay of Δ time.

Another important aspect of time critical behaviour of real-time systems is time dependency, which says that the time constraints of some actions depends on the happening time of preceding actions. For example, consider a machine which can perform action a followed by action b. Action b causally depends on action a. There is at least a delay of time Δ between the occurrences of a and b, and the machine must perform both actions a and b within 25 seconds.

In this thesis, we study the possibility of incorporating time explicitly to the well developed techniques, such as synchronisation trees and process algebras, to reason about quantitative as well as qualitative timing behaviour of systems. We first present a general model, Timed Synchronisation Trees, for Real-Timed Calculi. Timed synchronisation trees are extensions of synchronisation trees with time. We make no assumption about the underlying nature of time, allowing time to be discrete (such as the natural numbers ) or dense (such as the nonnegative rationals ^{≥0} or the non-negative reals ^{≥0}). All constructions on timed synchronisation trees are continuous with respect to a natural complete partial order of timed synchronisation trees. This allows timed synchronisation trees to be used to define denotational semantics for a wide range of timed calculi.

We also present a timed calculus, Timed CCS, which is an extension of Milner’s CCS with time. We again make no assumption about the underlying nature of time, allowing it to be discrete or dense. Atomic actions take no time, i.e. they are instantaneous. This assumption is essential if we are to use an interleaving model for real-time systems. For an asynchronous system, any two events which are not causally related or in conflict may occur not at the same time but at times which are arbitrarily close to each other. We say two events occur at the same time if one follows the other without any non-zero delay between them. However, this assumption also means that we can define processes (usually called the Zeno machines) which perform an infinite sequence of events in finite time or perform infinite events without time progress. To be more realistic, we may insist that for any two events which are causally related there should be some non-zero constant delay between them. This may be understood as saying that every action has a non-zero constant duration. We have no such realistic assumption when we develop the theory of Timed CCS and try to keep the calculus as general as possible. It is a task for the user to write realistic processes.

Postulating that every atomic action has a non-zero constant duration allows the usual notions of causality, concurrency and conflict to be observed within Timed CCS in the following sense:

- two events are causally related if both of them can occur in the same run but never at the same time, where we say two events can occur in the same run if one event occurs first and then, after a sequence of events, the other event can occur;

- two events are in the concurrency relation if they can occur at the same time;

- two events are in the conflict relation if they cannot both occur in the same run.

We satisfy this condition (that every atomic action has a non-zero constant duration) by saying that for any two events which are causally related there should be at least some non-zero constant delay between them. We can interpret CCS processes within Timed CCS based on this postulation. As a consequence, we obtain a partial order or true concurrency semantics for CCS. Since Timed CCS is an interleaving model, we in fact develop a partial order or true concurrency semantics based on an interleaving model.

In the remainder of this introduction, we briefly outline the background knowledge and references for our study before giving an outline of the thesis.

1.1 Background

1.1.1 CCS

Process algebras like Milner’s Calculus of Communicating Systems (CCS) [Mil80, Mil89a], Hoare’s Communicating Sequential Processes (CSP) [BHR84,Hoa85] and Bergstra and Klop’s Algebra of Communicating Processes (ACP) [BK84,BK85] view concurrent systems as structured entities which interact via synchronisation mechanisms. Among these process algebras, we regard here Milner’s CCS as a standard representative. In CCS, agents (or processes) are able to perform actions and their complementary co-actions. A synchronisation between agents is achieved when a pair of complementary actions occur simultaneously. The result of a synchronisation is to eliminate the (action, co-action) pair and replace it by a silent τ action.

The Language

To give a formal description of the syntax of CCS, we presuppose a set Λ of action names which does not contain τ, ϵ, and is ranged over by a, b, c, possibly indexed. Let Act = Λ ∪ {τ} which is ranged over by α, β. We also presuppose a structure on Λ that it can be partitioned into Γ, the set of names, and \overline{Γ} = \{ā : a ∈ Γ\}, the set of co-names, with the provision that ¯ ā = a. We call actions a and ā a pair of complementary actions which forms the basis of communications in CCS. Let V_{p} be an infinite set of process variables, ranged over by X, Y. The process expressions of CCS, ranged over by E, F, is defined by the following BNF expression:

E ::= X |nil |α.E |E + F |E | F |E\a |E[S] |μX.E

where S : Λ⟶Λ is a relabelling function which satisfies \overline{S(a)} = S(ā). By convention, we have S(τ) = τ.

The process nil cannot perform any action. The prefix α.E represents a process which can perform action α. After doing so, it becomes the process E. We will often omit the “nil” in the term “α.nil”. Also, we will often drop the “.” of “α.E”. For example, we render a.b.nil + b.a.nil as ab + ba. The summation E + F represents a process which can behave as process E or process F. The choice is made at the time of the first action of E or F. Process E | F represents parallel composition of processes E and F. Both E and F proceed independently. Synchronisation may occur when they perform a pair of complementary actions representing communication between them. The restriction E\a represents a process which behaves as process E except that action a and its complementary action ā are forbidden. Relabelling E[S] represents the process derived from process E by relabelling its action using the relabelling function S. Process μX.E is an infinite process which is defined by an equation X = E. The operator μX in process μX.E binds all free occurrences of process variable X in process E. This give us in the usual sense the notions of free and bound occurrences of process variables. We say a process is an agent if it does not contain any free occurrence of process variables. We usually use P to represent the set of all agents, ranged over by P, Q.

Transition Systems

The operational semantics of CCS is given in terms of labelled transition systems, which are a general model of computation described in [Kel76]. A labelled transition system is a pair (S, {⟶^{t} : t ∈ T }) where S is a set of states, T is a set of transition labels and ⟶^{t} ⊆ S × S is a transition relation (for every t of T). For convenience, we write s⟶^{t}s′ in place of (s, s′) ∈ ⟶^{t}. Intuitively, a transition of the form s⟶^{t}s′ indicates that the system, when in state s, may perform action t and in so doing evolves to state s′.

The operational semantics of CCS is defined by transition relations of the

\overline{α.P ⟶^{α}P}

\frac{P ⟶^{α}P′}{P + Q⟶^{α}P′}  \frac{P ⟶^{α}P′}{Q + P ⟶^{α}P′}
\frac{P ⟶^{α}P′}{P | Q⟶^{α}P′ | Q}  \frac{P ⟶^{α}P′}{Q | P ⟶^{α}Q | P′}

\frac{P ⟶^{a}P′, Q⟶^{ā}Q′}{P | Q⟶^{τ}P′ | Q′}

\frac{P ⟶^{α}P′}{P \a⟶^{α}P′\a} a ≠ α ∧ ā ≠ α

\frac{P ⟶^{α}P′}{P [S]⟶^{S(α)}P′[S]}

\frac{E\{μX.E/X\}⟶^{α}P}{μX.E⟶^{α}P}

Table 1–1: Operational Rules for CCS

form P ⟶^{α}Q of Plotkin’s Structured Operational Semantics (SOS) [Plo81] style. Table 1–1 presents all transition rules, which are in natural deduction style and have the following form:

\frac{T_{1}, ⋯, T_{n}}{T}

Transition rules of the above form have the following interpretation: T is derivable if all T_{1}, ⋯, T_{n} are derivable.

A transition T is allowed if and only if it can be derived by using the transition rules of Table 1–1. The operational semantics of CCS is given by the least transition relations ⟶^{α}, where α ∈ Act, defined in Table 1–1.

Synchronisation Trees

Synchronisation trees [Mil80,Win84a] are a concrete model for much of the work on concurrency. They are trees with the vertices representing states and edges labelled by actions which show how to synchronise with the environment.

If we collect the derivatives of a CCS agent P into a tree form, we get a derivation tree of P. For example, the derivation tree of CCS agent a(b + c) is presented in Figure 1–1. The derivation trees of CCS agents correspond to synchronisation trees.

[figure: b; nil; c; nil; b + c; a; a(b + c)]

Figure 1–1: The Derivation Tree of a(b + c)

By introducing an appropriate ordering on synchronisation trees, we get a complete partial order of such structures. Furthermore, natural constructions defined over such trees are continuous with respect to this ordering, so we can naturally define infinite synchronisation trees. As a result we can give a denotational semantics for CCS based on synchronisation trees [Win84a].

Bisimulations

A more abstract semantics for CCS is achieved by identifying those agents which cannot be distinguished by any external observation of their behaviour. A notion of bisimulation [Mil89a,Par81] is a standard device for defining behavioural equivalence for process algebras.

We say a binary relation R over agents is a strong bisimulation if for any agents P and Q, (P, Q) ∈ R implies that for any α ∈ Act,

(1) whenever P ⟶^{α}P′, then Q⟶^{α}Q′ and (P′, Q′) ∈ R for some Q′;

(2) whenever Q⟶^{α}Q′, then P ⟶^{α}P′ and (P′, Q′) ∈ R for some P′.

Two agents P and Q are strongly bisimilar, written P ∼ Q, if there is a strong bisimulation which contains (P, Q). The relation ∼ itself is a strong bisimulation, the largest strong bisimulation. It is an equivalence relation, called strong equivalence. Moreover it is a congruence relation, i.e. it is substitutive for all operators including recursive operator.

Strong bisimulation treats the internal action τ in the same way as all other actions and requires every τ action in one agent be matched by a τ action in the other. By relaxing the requirement and allowing a τ action to be matched by zero or more τ actions, we obtain the notion of weak bisimulation.

Let τ̂ be ϵ and â, where a ∈ Λ, be a. We write P ⟹^{ϵ}P′ in place of P (⟶^{τ})^{∗}P′ and P ⟹^{α}P′ in place of P (⟶^{τ})^{∗} · ⟶^{α} · (⟶^{τ})^{∗}P′. Note that for every CCS agent P, we have P ⟹^{ϵ}P. A binary relation R over agents is a weak bisimulation if (P, Q) ∈ R implies that for any α ∈ Act,

(1) whenever P ⟶^{α}P′, then Q⟹^{α̂}Q′ and (P′, Q′) ∈ R for some Q′;

(2) whenever Q⟶^{α}Q′, then P ⟹^{α̂}P′ and (P′, Q′) ∈ R for some P′.

Similarly two agents P and Q are weakly bisimilar, written P ≈ Q, if there is a weak bisimulation containing (P, Q). The relation ≈ itself is a weak bisimulation, the largest weak bisimulation. Moreover it is an equivalence relation, but not a congruence relation. In general, the summation operator does not preserve weak bisimilarity. For example, a ≈ τa but a + b ≉ τa + b.

Since the relation ≈ is not preserved by summation, we define a relation =^{+} by saying that P =^{+} Q if P + R ≈ Q + R for any agent R. The relation =^{+} is a congruence relation. In fact it is the largest congruence relation contained in weak equivalence ≈.

1.1.2 Hennessy-Milner Logic

An alternative characterization of bisimulation is given by Hennessy and Milner [HM85] based on a simple modal logic which is often referred to as Hennessy-Milner Logic. This further confirms the naturalness of the notion of bisimulation.

The formulas of Hennessy-Milner logic, ranged over by φ, ψ, are defined by the following BNF expression:

φ ::= tt | ¬φ | φ ∧ ψ | ⟨a⟩φ

where a ∈ A. The formula ⟨a⟩φ is called a modalized formula with the intended meaning that after some a action φ holds. The class of modalized formulas is parameterized by a label set A. So the class of transition systems over a given label set has a Hennessy-Milner logic associated with it.

The formulas of Hennessy-Milner logic are interpreted over a transition system of the form (S, {⟶^{a} : a ∈ A}). As CCS defines a transition system (P, {⟶^{α} : α ∈ Act}), the formulas of Hennessy-Milner logic can be interpreted over CCS as follows:

(1) for every agent P, we have P ⊧ tt;

(2) P ⊧ ¬φ if and only if not P ⊧ φ;

(3) P ⊧ φ ∧ ψ if and only if P ⊧ φ and P ⊧ ψ;

(4) P ⊧ ⟨α⟩φ if and only if there is a transition P ⟶^{α}P′ such that P′ ⊧ φ.

An important derived operator is [α], the dual of ⟨α⟩, i.e. [α]φ =^{def} ¬⟨α⟩¬φ. The formulas of Hennessy-Milner logic can be used to specify the desired properties of a nondeterministic or concurrent system. As an example, consider the vending machine V of [Mil89a] where

V =^{def} 2p.big.collect.V + 1p.little.collect.V

We can specify the following interesting properties of vending machine V:

1. after 2p is deposited, only the big button can be pressed

V ⊧ [2p]([little]ff ∧ ⟨big⟩tt)

2. after 1p is deposited and the little button is pressed, a chocolate can be

collected

V ⊧ [1p][little]⟨collect⟩tt

In order to support modular design and verification, a problem of compositionality of modal assertions has been raised. This problem has been successfully dealt with by the works of [Sti87,Win84b,LL90] for CCS and SCCS. In [Lar88, Cle90,BS92,SW89,Win89], proof systems, tableau methods and rewrite rules for Hennessy-Milner logic with recursion have been proposed. This allows us to reason about temporal properties of processes which are to hold invariantly or eventually.

1.1.3 Labelled Event Structures

Labelled event structures [NPW81,Win87] represent processes by means of events together with a relation of conflict, which describes how occurrences of certain events exclude others, and a relation of enabling, which describes how events are causally related. Events may occur concurrently if they are not in conflict or enabling relations. The concurrency relation between events is presented by the absence of the conflict and enabling relations.

An A-labelled event structure is a quadruple S = (E, ≺, #, ℓ) where - (E, ≺) is a partial ordering of events, where ≺ is called the causality or precondition relation, such that for every e ∈ E, the set {e′ ∈ E : e′ ≺ e} is finite;

- #, the conflict relation, is a symmetric and irreflexive binary relation on E which is hereditary in the sense that if e_{1}#e and e ≺ e_{2} then e_{1}#e_{2}; and

- ℓ : E⟶A is a labelling function from events to actions.

Two events of E are in the concurrency relation if they are neither in the causality relation nor in the conflict relation. The concurrency relation is a symmetric and irreflexive binary relation of E and the causality, conflict and concurrency relations form a partition of E × E.

For any A-labelled event structure S = (E, ≺, #, ℓ), a subset F ⊆ E of events is said to be a configuration or computation of S if F is conflict free and closed under preconditions. As the conflict relation # is irreflexive and hereditary, a configuration is conflict free, i.e. for any events e and e′ of a configuration, relation e#e does not hold. Viewing computations of an A-labelled event structure as such subsets of events, progress in a computation can be measured by the occurrence of more events. Denoting the set of all computations of S by E(S), we know that (E(S), ⊆) is a domain which enjoys many nice properties [Win87].

Labelled event structures are used to provide true concurrency semantics for process algebras. In [Win83], a denotational semantics of CCS based on labelled event structures has been proposed. However, the labelled event structure semantics is still very intensional (similar to the interleaving approach). Some notions of equivalence for event structures which preserve concurrency have been proposed in the literature. These include Boudol and Castellani’s pomset bisimulation [BC87,BC89] and Degano, De Nicola and Montanari’s partial order bisimulation [DDM89].

1.2 Layout of the Thesis

In Chapter 2, we present a mathematical model, timed synchronisation trees, for timed calculi. A timed synchronisation tree is a rooted tree with vertices representing states and edges labelled by actions to show how to synchronise with the environment. The vertices are labelled by time information which shows the maximal delay time of the vertices and the time constraints over actions labelling the path from the root to the vertices. All constructions of timed synchronisation trees are continuous with respect to a natural complete partial order. This allows us to recursively define infinite timed synchronisation trees along standard lines. Since trees are concrete interleaving models, we define an equivalence relation on timed synchronisation trees based on a notion of behaviour of timed synchronisation trees.

In Chapter 3, we give a formal description for Timed CCS, including its syntax and semantics. We present its operational and denotational semantics. The operational semantics is in Plotkin’s SOS style and the denotational semantics is based on timed synchronisation trees. Time variables in the language allow us to express the notion of time dependency. We also introduce some derived operators which will be used in the thesis. We present three examples to show the utility of the calculus for the specification and verification of real-time systems. The examples illustrate three important aspects of real-time systems, i.e. time out, duration control and time dependency. In this chapter, we also discuss our decisions on the design of the calculus and compare it with related work.

In Chapter 4, we extend the notion of strong bisimulation to timed processes and show that strong equivalence enjoys many desirable properties including an expansion law. Strong equivalence is a congruence relation. We show the two semantics (operational and denotational) of Timed CCS are identical in the sense that the equivalences on Timed CCS induced by the denotational and operational semantics coincide. Equations which satisfy some condition are shown to have unique solutions up to strong equivalence. We also present a simple modal logic which is an extension of Hennessy-Milner logic with time and show a modal characterization of strong bisimulation. This not only shows that bisimulation is a natural equivalence, but also suggests that modal logic is an appropriate program logic for the specification and verification of real-time systems.

In Chapter 5, we show that strong equivalence is decidable for finite processes, i.e. those processes without recursion. The decidability is independent of the choice of time domain, allowing time to be discrete or dense.

In Chapter 6, we present a simple proof system for strong equivalence. The proof system is also independent of the choice of time domain. It is sound and complete for finite processes over dense time domains, but only complete for a restricted language over discrete time domains. We show by an example how the proof system works for recursively defined processes.

In Chapter 7, we discuss behavioural abstraction of timed processes. As in CSS, weak bisimulation in Timed CCS is not fully substitutive. It is not preserved by the summation operator. We refine weak bisimulation and define an observational congruence relation which is the largest congruence relation included in weak bisimulation. We show that equations which satisfy some conditions have unique solutions up to observational congruence.

In Chapter 8, we show that if we postulate that every atomic action has a nonzero constant duration (we satisfy this by saying that for any two events which are causally related there should be at least a non-zero constant delay between them), then we can observe the causality relation in real-time calculi. We interpret CCS processes within Timed CCS based on a postulation that for any two events which are causally related there is at least a delay Δ (where Δ > 0) between them. As a result, we obtain a timed semantics for CCS. The time semantics of CCS is a partial order or true concurrency semantics. We in fact develop a partial order or true concurrency semantics for CCS based on an interleaving approach.

In Chapter 9, we summerise the thesis and discuss future research topics and directions.

Timed Synchronisation Trees

Tree semantics arise naturally when concurrency is simulated by nondeterministic interleaving. In [Mil80], Milner uses synchronisation trees as an interleaving model for parallel computation in which processes communicate by mutual synchronisation. By further labelling the vertices of synchronisation trees with time constraints, we obtain timed synchronisation trees. The time constraints associated with the vertices of trees represent the maximal delay time of the vertices and the time at which the actions labelling the paths from the root to the vertices can occur in order to arrive at the vertices. Timed synchronisation trees are a general interleaving model of real-time systems in which processes communicate by mutual synchronisation, analogous to synchronisation trees. For example, the following tree

[figure: {(t, t′)|t ≥ 0&0 ≤ t′ ≤ t}; b; {t|t ≥ 0}; a]

can be used to express a machine which can first perform action a at time t, where t ≥ 0, and after doing so it can perform action b at a relative time t′, where 0 ≤ t′ ≤ t. However, in real-time systems, one important notion is time out. There are lower and upper bounds on when events can occur relative to the other events. Consider a machine M which can perform action a or b, but not both. Action a and b can occur before 10 minutes. If a and b do not occur, then the machine M evolves to a dead state after a delay of 10 minutes. To express the machine M, we need to represent a notion of the maximal delay time of a state of a machine. For example, the following tree can be used to represent the machine M:

[figure: 0; a; 10; b; 0; {t|0 ≤ t < 10}; {t|0 ≤ t < 10}]

2.1 A Description of the Model

In this section, we give a formal description of the timed synchronisation trees.

2.1.1 Timed Synchronisation Trees

Timed synchronisation trees are certain kinds of rooted trees. The vertices of trees represent states and the edges represent event occurrences which cause changes of states. Edges and vertices are both labelled. The edges are labelled by elements of a nonempty set A of actions, which the machine under consideration may perform. The labels over edges show how the machine synchronises with the environment. The vertices are labelled with time constraints which express the maximal delay time of the machine at the vertices and time at which the actions labelling the path from the root to the vertices can happen in order to arrive at the vertices. To define timed synchronisation trees, we first define graphs.

Definition 2.1.1 A graph G is a pair (V, E), where V is a set of vertices and E, a subset of the set of unordered pairs of V, is a set of edges.

An edge ⟨v, v′⟩ joins the vertices v and v′, which in turn are called the endvertices of ⟨v, v′⟩. Two edges are adjacent if they have exactly one common endvertex. A path between vertices v_{1} and v_{n+1} in G is a sequence of edges e_{1}, ⋯, e_{n} of G, where e_{1} = ⟨v_{1}, v_{2}⟩, ⋯, e_{n} = ⟨v_{n}, v_{n+1}⟩ are all distinct. The length of a path p is the length of the sequence p. A path p in G is a cycle if its length is not 0 and it is a path between a vertex v and itself.

Definition 2.1.2 A tree is a graph (V, E) with a special vertex r ∈ V, the root of the tree, such that

(1) for any v ∈ V there is a path between r and v;

(2) there are no cycles in (V, E).

Note that a tree contains at least one vertex, the root of the tree. We use (V, E, r) to represent a tree with the set V of vertices, the set E of edges and the root r. The height of a vertex v of a tree (V, E, r), written h(v), is defined to be the length of the path between v and r.

Definition 2.1.3 An A-labelled tree is a tree (V, E, r) together with a labelling function l : E ⟶ A.

We use (V, E, r, l) to represent an A-labelled tree with the tree (V, E, r) and the labelling function l : E ⟶ A.

For convenience, we will say a labelled tree instead of an A-labelled tree when A is clear from the context.

To define timed synchronisation trees, we presuppose a time domain (T ∪ {∞}, ≤ ), where T contains a least element 0 which represents the starting time and ≤ is a linear order over T . We introduce an infinite time ∞, ∞ ∉ T , which satisfies that u ∈ T implies u ≤ ∞. We make no assumption about the underlying nature of time, allowing T to be discrete, such as (the set of natural numbers), or dense, such as ^{≥0} (the non-negative rationals) or ^{≥0} (the non-negative reals).

Notation

(1) D^{0} =^{def} T ∪ {∞}

(2) D^{i} =^{def} 2^{T^{i}×D^{0}} where i ∈ − {0}

where T^{i} represents \underbrace{T × ⋯ × T}_{i}. □

Let D^{∗} represent the set ⋃_{i∈ω} D^{i}. For any set S, we will write S_{⊥} in place of S∪ {⊥}. We will sometime abuse notations and write ((u_{1}, ⋯, u_{n}), u) as (u_{1}, ·, u_{n}, u).

Definition 2.1.4 A timed A-labelled tree is a labelled tree (V, E, r, l) together with a time function t which assigns to every vertex v of height n an element of D_{⊥}^{n} such that

(1) if t(v) = ⊥ and ⟨v, v′⟩ ∈ E, where h(v′) = h(v) + 1, then t(v′) = ⊥. Vertices labelled by ⊥ are called open vertices.

(2) if ⟨v, v′⟩ ∈ E, where h(v′) = h(v) + 1, and vertex v′ is not an open vertex, then for any ((u_{1}, ⋯, u_{n}), u) ∈ t(v′), there is a u′ ∈ D^{0} such that u_{n} ≤ u′ and ((u_{1}, ⋯, u_{n−1}), u′) ∈ t(v).

Elements of D_{⊥}^{∗} which are associated to vertices of a labelled tree record time constraints over actions labelling paths from the root to the vertices and the maximal delay time of the vertices. For example, if a path between the root and a vertex v are labelled by action a_{1}, ⋯, a_{n} and an element of D_{⊥}^{∗} labelling v contains ((u_{1}, ⋯, u_{n}), u), then to arrive at v, action a_{i} may occur at time u_{i} relative to the previous action, where i = 1, ⋯, n. When the machine arrives at

[figure: v_{1}; v_{2}; v_{0}; a; b; c; v_{3}]

Figure 2–1: Labelled Tree T

v, its maximal delay time is u. We understand a timed labelled tree by the idea that its vertices represent states and its edges represent event occurrences. The vertices are labelled by the elements of D_{⊥}^{∗} which show time constraints over the actions labelling the paths from the root to the vertices and the maximal delay time of the vertices. The edges are labelled to show how to synchronise with the environment.

Open vertices describe parts of machines which are not fully defined. Time constraints associated to those open vertices cannot be elaborated. As a consequence, the successor vertices of open vertices must also be open vertices which is shown by condition (1). Condition (2) represents that time constraints associated to vertices which are in the same path starting from the root must satisfy a consistency condition. This consistency condition may be understood as: if vertices v and v′ are connected by an edge ⟨v, v′⟩, where h(v) + 1 = h(v′), and ((u_{1}, ⋯, u_{n}), u) ∈ t(v′); let a_{1}, ⋯, a_{n−1} label the path from the root r to v and a label the edge ⟨v, v′⟩, then a_{1}, ⋯, a_{n−1} and a may happen at times u_{1}, ⋯, u_{n−1} and u_{n}, respectively. When the machine is in the state v, it may delay at least time u_{n} before action a, as action a occurs at time u_{n}. So we have ((u_{1}, ⋯, u_{n−1}), u′) ∈ t(v) for some u′ ≥ u_{n}.

For example, the labelled tree T of Figure 2–1 with a time function t, where t(v_{0}) = 15, t(v_{1}) = {(2, 5)}, t(v_{2}) = {(15, 0)} and t(v_{3}) = {((5, 6), 0)}, is not a timed labelled tree, as the time information tells us that to arrive at v_{1} action a must occur after a delay of time 2 and to arrive at v_{3} (note that to arrive at v_{3}, we must first arrive at v_{1}), action a must occur after a delay of time 5 and then action c occurs after another delay of time 6, a contradiction. Similarly, the labelled tree T with a time function t′, where t′(v_{0}) = 3, t′(v_{1}) = {(10, 5)}, t(v_{2}) = {(15, 0)} and t′(v_{3}) = {(10, 6, 0)}, is also not a timed labelled tree, as the time information tells us that the machine (we assume that the machine starts from v_{0}) can delay at most time 3 but action a can occur after a delay of time 10, a contradiction.

We write v→^{a}_{T} v′ to represent the edge of a tree T between v and v′ which is labelled by a, where h(v) + 1 = h(v′). We use P(T) to represent the set of all paths starting from the root of T. By convention, we use V, E, r, l and t to represent the sets of vertices and edges, the root, the labelling function and the time function of a timed labelled tree T, respectively.

Since an experimenter cannot see the states (only event occurrences can be observed from outside), we identify those timed labelled trees which are the same up to changes of the names of the vertices.

Definition 2.1.5 Two timed labelled trees T = (V, E, r, l, t) and T′ = (V′, E′, r′, l′, t′) are isomorphic, written as T = T′, if there is a bijective map f : V ⟶ V′ such that

(1) f(r) = r′;

(2) v→^{a}_{T} v′ if and only if f(v)→^{a}_{T′}f(v′); and

(3) t = f ∘ t′.

Our timed synchronisation trees are isomorphism classes of timed labelled trees.

[figure: u_{2} = 10 − u_{1}^{2≤u_{1}≤10}; u_{2} = ∞^{5≤u_{1}≤12}; ∞; a; b; c; u_{3} = ∞^{0≤u_{2}≤10−u_{1}}^{2≤u_{1}≤10}]

Figure 2–2: Timed Synchronisation Tree T

Definition 2.1.6 A timed synchronisation tree T = [V, E, r, l, t] is an isomorphism class of a timed labelled tree (V, E, r, l, t).

Let Ts represent the set of all timed synchronisation trees, ranged over by T. For any timed synchronisation tree [V, E, r, l, t], we regard the labelled tree (V, E, r, l) as its underlying tree structure.

The timed synchronisation trees are an interleaving model of real-time systems. For example, the timed synchronisation tree T of Figure 2–2, where 2 ≤ u_{1} ≤ 10, 0 ≤ u_{2} ≤ 10 − u_{1} and u_{3} = ∞ stand for the set {(u_{1}, u_{2}, u_{3}) : 2 ≤ u_{1} ≤ 10 & 0 ≤ u_{2} ≤ 10 − u_{1} & u_{3} = ∞}, represents a machine which can perform either an action a followed by an action c or an action b, but not both. Action a can happen between 2 seconds and 10 seconds (if we measure time in seconds). If action a happens at time u (2 ≤ u ≤ 10), then action c can happen within another 10 − u seconds (inclusive). Note that the time constraints of action c depend on the happening time of action a. This represents the notion of time dependency of real-time systems. Action b may happen between 5 seconds and 12 seconds. After c or b happens, the machine evolves to a state in which no actions can occur, but time may proceed indefinitely. If a and b do not occur after a delay of 15 seconds, the machine will evolve to a state in which the machine cannot perform any action but lets time proceed.

2.1.2 A Complete Partial Order over Ts

In this section, we define a natural CPO on timed synchronisation trees.

A partially ordered set is a set D together with a binary relation ⊑_{D} over D which is reflexive, antisymmetric and transitive. We usually write D for the partially ordered set (D, ⊑_{D}) when the ordering ⊑_{D} is clear from the context. An ωchain of a partially ordered set D is an infinite sequence of elements, d_{0}, ⋯, d_{n}, ⋯, of D such that d_{i} ⊑_{D} d_{i+1} where i ∈ ω. An element ⊥_{D} in D is called a least element of D if it satisfies ⊥_{D} ⊑_{D} d for every d ∈ D. It follows from the antisymmetry of ⊑_{D} that if least elements exist, then they are unique. For any subset M of D, an element a is called an upper bound of M if for every d ∈ M we have d ⊑_{D} a. We say a is a least upper bound (lub) of M if it is an upper bound, and for any upper bound b of M we have a ⊑_{D} b. Similarly, if least upper bounds exist, then they are unique. We use ⊔_{D}M to represent the least upper bound of M in D, when it exists. For convenience, when D is understood from the context, we drop the subscript D.

A partially ordered set or partial order (D, ⊑) is complete, called a complete partial order (CPO), if it contains a least element ⊥ and any ω-chain d_{0}, ⋯, d_{n}, ⋯ of D has a least upper bound ⊔_{i∈ω}d_{i} (we write ⊔_{i∈ω}d_{i} for ⊔{d_{i} : i ∈ ω}).

Given two CPOs D and E, a function f : D ⟶ E is monotonic if for any d, d′ ∈ D, d ⊑ d′ implies f(d) ⊑ f(d′). If f is monotonic and for any ω-chain d_{0}, ⋯, d_{n}, ⋯ we have f(⊔_{i∈ω}d_{i}) = ⊔_{i∈ω}f(d_{i}), then we say f is continuous. We write [D ⟶ E] for the set of all continuous functions from D to E. For any f, g ∈ [D ⟶ E], we say f ⊑ g if and only if for every d ∈ D, f(d) ⊑ g(d). This ordering is usually known as the induced pointwise ordering. With this ordering, [D ⟶ E] itself is a CPO.

The following results are standard classical results of domain theory. For more details, the reader may refer to a standard reference [Hen88a].

Lemma 2.1.7 A function f : D ⟶ D′ is continuous if and only if it is monotonic and for every ω-chain d_{0}, ⋯, d_{n}, ⋯ of D

f(⊔_{i∈ω}d_{i}) ⊑ ⊔_{i∈ω}f(d_{i})

For any CPOs D_{1} and D_{2}, we define an ordering ⊑ on the Cartesian product of D_{1} and D_{2} as follows: for every ⟨d_{1}, d_{2}⟩ and ⟨d′_{1}, d′_{2}⟩ of D_{1} × D_{2}, ⟨d_{1}, d_{2}⟩ ⊑ ⟨d′_{1}, d′_{2}⟩ if both d_{1} ⊑ d′_{1} and d_{2} ⊑ d′_{2} hold. With this ordering, D_{1} × D_{2} is a CPO.

A function f : D_{1} × D_{2} ⟶ D is left-continuous if for every element d of D_{2} and every ω-chain ⟨d_{0}, d⟩, ⋯, ⟨d_{n}, d⟩, ⋯ of D_{1} × D_{2}

f(⊔_{i∈ω}⟨d_{i}, d⟩) = ⊔_{i∈ω}f(⟨d_{i}, d⟩)

Similarly we can define right-continuous function.

Lemma 2.1.8 A function f : D_{1} × D_{2} ⟶ D is continuous if and only if it is both left-continuous and right-continuous.

Definition 2.1.9 Let f ∈ [D ⟶ D]. An element d of D is called a fixpoint of f if d = f(d). It is a least fixpoint of f if it is a fixpoint of f and for any other fixpoint d′ of f, we have d ⊑ d′.

Obviously if a function f ∈ [D ⟶ D] has least fixpoints, then the least fixpoints are unique. Moreover continuous functions always have least fixpoints.

Theorem 2.1.10 Every f ∈ [D ⟶ D] has a least fixpoint.

Now we consider a natural CPO over timed synchronisation trees.

Let ⊑ be a partial order over D_{⊥}^{∗} satisfying that for any S, S′ ∈ D_{⊥}^{∗}, S ⊑ S′ implies S = ⊥ or S = S′. A partial order ⊑ over the set [V ⟶ D_{⊥}^{∗}] of continuous time functions is the induced pointwise ordering.

Definition 2.1.11 (A Partial Order over Ts) For any T, T′ ∈ T s, we say T ⊑ T′ if for any (V, E, r, l, t) ∈ T, there is a (V′, E′, r′, l′, t′) ∈ T′ such that

(1) V ⊆ V′  (4) l = l′|_{E}
(2) E ⊆ E′  (5) t ⊑ t′|_{V}
(3) r = r′

Note that for any function f, we use f|_{S} to represent the restriction of f to the set S.

Lemma 2.1.12 ⊑ is a partial order over Ts.

Proof: It is easy to show that ⊑ over Ts is reflexive, antisymmetric and transitive. □

Theorem 2.1.13 (T s, ⊑) is a CPO.

Proof: The timed synchronisation tree [{v}, ∅, v, ∅, {(v, ⊥)}] is the least element of Ts. For any ω-chain T_{0}, ⋯, T_{n}, ⋯, let (V_{i}, E_{i}, r_{i}, l_{i}, t_{i}) ∈ T_{i} such that V_{i} ⊆ V_{i+1}, E_{i} ⊆ E_{i+1} r_{i} = r_{i+1}, l_{i} = l_{i+1}|_{E_{i}} and t_{i} ⊑ t_{i+1}|_{V_{i}}, where i ∈ ω. We may show that

T = [∪_{i∈ω}V_{i}, ∪_{i∈ω}E_{i}, r_{0}, ⊔_{i∈ω}l_{i}, ⊔_{i∈ω}t_{i}]

is the least upper bound of the ω-chain.

We first need to show that T is a timed synchronisation tree.

(1) It is easy to check that

(∪_{i∈ω}V_{i}, ∪_{i∈ω}E_{i}, r_{0}, ⊔_{i∈ω}l_{i})

is a labelled tree.

(2) For any v ∈ ∪_{i∈ω}V_{i}, let n be the height of v. If ⊔_{i∈ω}t_{i}(v) ≠ ⊥, then there is an m such that for all i ≥ m, we have t_{i}(v) = t_{m}(v), where t_{m}(v) ∈ D^{n}. Hence ⊔_{i∈ω}t_{i}(v) ∈ D_{⊥}^{n}.

(3) Suppose ⊔_{i∈ω}t_{i}(v) = ⊥ and ⟨v, v′⟩ ∈ ⊔_{i∈ω}E_{i}, where h(v) + 1 = h(v′). Then for every i ∈ ω, v ∈ V_{i} implies t_{i}(v) = ⊥. Also there is an n such that for any i ≥ n, ⟨v, v′⟩ ∈ E_{i}. Hence for any i ≥ n, we have t_{i}(v′) = ⊥. Therefore ⊔_{i∈ω}t_{i}(v′) = ⊥.

(4) Let ⟨v, v′⟩ ∈ ∪_{i∈ω}E_{i} where h(v) + 1 = h(v′) and v′ is not an open vertex. Suppose (u_{1}, ⋯, u_{n}, u) ∈ ⊔_{i∈ω}t_{i}(v′). There is an n such that for any i ≥ n we have (u_{1}, ⋯, u_{n}, u) ∈ t_{i}(v′). So for any i ≥ n, there is a u′ such that u′ ≥ u_{n} and (u_{1}, ⋯, u_{n−1}, u′) ∈ t_{i}(v). Therefore (u_{1}, ⋯, u_{n−1}, u′) ∈ ⊔_{i∈ω}t_{i}(v).

Now we only need to show that T is the least upper bound of the ω-chain, which directly follows from the definition of ⊑ over Ts. □

2.2 Constructions

In this section, we consider some constructions over Ts.

2.2.1 Empty Constant

Let Ω be the timed synchronisation tree [{v}, ∅, v, ∅, {(v, ⊥)}], which is the least element of Ts. We call it the empty constant. The empty element may be described diagrammatically as:

• ⊥

2.2.2 Prefix

To capture the notion of time dependency, we define a time synchronisation tree with a parameter as an isomorphism class of a labelled tree T with a time function which assigns to every vertex v of depth i a function f_{v} : T ⟶ D_{⊥}^{i} such that if v →_{T} v′ then for any u ∈ T , f_{v}(u) and f_{v′}(u) satisfy conditions (1) and (2) of

[figure: u_{2} = 10 − u_{1}^{2≤u_{1}≤10+x}; u_{2} = ∞^{5≤u_{1}≤12+x}; 15 + x; a; b; c; u_{3} = ∞^{0≤u_{2}≤10−u_{1}}^{2≤u_{1}≤10+x}]

Figure 2–3: Timed Synchronisation Tree T with Parameter x

Definition 2.1.4. A timed synchronisation tree with a parameter x can be regarded as a family of timed synchronisation trees which are indexed by the parameter x. All timed synchronisation trees in the family have the same underlying tree structure, i.e. they represent the same labelled tree if we ignore their time function, and only time constraints associated to every vertex may contain the parameter x. For example, Figure 2–3 represents a timed synchronisation tree with a parameter x. If we take x to be 0, then we get the timed synchronisation tree of Figure 2–2. We use T {u/x} to represent the timed synchronisation tree resulted by taking the parameter x to be u in T.

We can generalise the notion of timed synchronisation trees with a parameter to a notion of timed synchronisation trees with a sequence of parameters. As a special case, a timed synchronisation tree is a timed synchronisation tree with an empty sequence of parameters. Clearly a timed synchronisation tree with n parameters can also be regarded as a timed synchronisation tree with n + 1 parameters.

Definition 2.2.1 For any a ∈ A, S ⊆ T which has a least upper bound in T , and timed synchronisation tree T, possibly with parameters, the prefix a(S).(λx.T) represents a new timed synchronisation tree T′, possibly with parameters, such that

• V′ = {a} ⊎ V

[figure: 15; a; u_{3} = 10 − u_{1}^{2≤u_{2}≤10+u_{1}}^{0≤u_{1}≤15}; u_{3} = ∞^{5≤u_{2}≤12+u_{1}}^{0≤u_{1}≤15}; u_{2} = 15 + u_{1}^{0≤u_{1}≤15}; a; b; c; u_{4} = ∞^{0≤u_{3}≤10−u_{2}}^{2≤u_{2}≤10+u_{1}}^{0≤u_{1}≤15}]

Figure 2–4: Timed Synchronisation Tree: a([0, 15])(λx.T)

• E′ = {⟨(v, 1), (v′, 1)⟩ : ⟨v, v′⟩ ∈ E} ⊎ {⟨(a, 0), (r, 1)⟩}

• r′ = (a, 0)

• l′ = λ(e, i). \{ \begin{matrix}a & i = 1&e = ⟨(a, 0), (r, 1)⟩ \\ l(⟨v, v′⟩) & i = 0&e = ⟨(v, 1), (v′, 1)⟩ \end{matrix}

• t′ = λ(v, i). \{ \begin{matrix}Sup(S) & (v, i) = r′ \\ ⊥ & t_{u}(v) = ⊥ \\ & where t_{u}(v) = (t\{u/x\})(v) & u ∈ S \\ \{⟨u⟩s : u ∈ S ∧ s ∈ t_{u}(v)\} & otherwise \end{matrix}

where Sup(S) represents the least upper bound of S. By convention, Sup(∅) = 0.

Note that we use λx.T in the prefix a(S)(λx.T) to emphasize the parameter x of T which will be instantiated next.

Figure 2–4 shows the result of prefixing the timed synchronisation tree T, with a parameter x, of Figure 2–3 with an action a and an interval [0, 15].

We still use Ts to represent the set of all timed synchronisation trees, possible with parameters. Let ⊑ over timed synchronisation trees with parameters be the induced pointwise ordering, i.e. for any timed synchronisation trees T and T′, where T and T′ contain at most parameters x_{1}, ⋯, x_{n}, we say T ⊑ T′ when T {u_{1}/x_{1}, ⋯, u_{n}/x_{n}} ⊑ T′{u_{1}/x_{1}, ⋯, u_{n}/x_{n}} for any u_{1}, ⋯, u_{n} ∈ T .

Theorem 2.2.2 a(S) : T s ⟶ T s is continuous with respect to ⊑.

Proof: Since the partial order ⊑ over timed synchronisation trees with parameters is the induced pointwise ordering, we only need to consider the case where T contains at most one parameter x. We use [a(S).V, a(S).E, a(S).r, a(S).l, a(S).(λx.t)] to represent the timed synchronisation tree a(S).(λx.T). It is easy to check that a(S) is monotonic. Now we only need to show that for any ω-chain T_{0}, ⋯, T_{n}, ⋯, we have

a(S).(∪_{i∈ω}V_{i}) ⊆ ∪_{i∈ω}a(S).V_{i}
a(S).(∪_{i∈ω}E_{i}) ⊆ ∪_{i∈ω}a(S).E_{i}
⊔_{i∈ω}a(S).l_{i} = a(S).(⊔_{i∈ω}l_{i})|_{a(S).(⊔_{i∈ω}E_{i})}

and

a(S).(⊔_{i∈ω}λx.t_{i}) ⊑ ⊔_{i∈ω}a(S).(λx.t_{i})|_{a(S).(⊔_{i∈ω}V_{i})}

We only consider the last one, as all others are similar.

For any v ∈ ∪_{i∈ω}V_{i}, if (a(S).(⊔_{i∈ω}λx.t_{i}))(v) = ⊥ then (a(S).(⊔_{i∈ω}λx.t_{i}))(v) ⊑ (⊔_{i∈ω}a(S).(λx.t_{i}))(v). Suppose (a(S).(⊔_{i∈ω}λx.t_{i}))(v) ≠ ⊥. If v is the root, then (a(S).(⊔_{i∈ω}λx.t_{i}))(v) = Sup(S) = (⊔_{i∈ω}a(S).(λx.t_{i}))(v). Now we also suppose v is not the root. Let s ∈ (a(S).(⊔_{i∈ω}λx.t_{i}))(v), then there is a s′ and u ∈ S such that s = ⟨u⟩s′ and s′ ∈ (⊔_{i∈ω}(t_{i}{u/x}))(v). Hence there is a k such that for any i ≥ k, s′ ∈ t_{i}{u/x}(v) and s ∈ (a(S).(λx.t_{i}))(v). So s ∈ (⊔_{i∈ω}a(S).(λx.t_{i}))(v). □

2.2.3 Summation

The sum of two timed synchronisation trees T and T′ represents a new timed synchronisation tree resulted by putting T and T′ together at their roots. Figure 2– 5 diagrammatically describes the summation operation.

[figure: u; T; +; T′; u′; T; T′; max(u, u′)]

Figure 2–5: Summation Operation

Definition 2.2.3 For any timed synchronisation trees T_{1} and T_{2}, possibly with parameters, T_{1} + T_{2} represents a new timed synchronisation tree T, where

• V = (V_{1} − {r_{1}}) ⊎ (V_{2} − {r_{2}}) ⊎ {(r_{1}, r_{2})}

• E = {⟨(v, 0), (v′, 0)⟩ : v ≠ r_{1}&⟨v, v′⟩ ∈ E_{1}} ⊎ {⟨(v, 1), (v′, 1)⟩ : v ≠ r_{2}&⟨v, v′⟩ ∈ E_{2}}

⊎ {⟨((r_{1}, r_{2}), 2), (v, i)⟩ : ⟨r_{i+1}, v⟩ ∈ E_{1} ∨ ⟨r_{i+1}, v⟩ ∈ E_{2}}

• r = ((r_{1}, r_{2}), 2)

• l = λ(e, i). \{ \begin{matrix}l_{1}(⟨v, v′⟩) & i = 0&e = ⟨(v, 0), (v′, 0)⟩ \\ l_{2}(⟨v, v′⟩) & i = 1&e = ⟨(v, 1), (v′, 1)⟩ \\ l_{j+1}(⟨r_{j+1}, v⟩) & i = 2&e = (r, (v, j))&v ∈ V_{j+1}&j = 0, 1 \end{matrix}

• t = λ(v, i). \{ \begin{matrix}max(t_{1}(r_{1}), t_{2}(r_{2})) & (v, i) = r \\ t_{i}(v) & v ∈ V_{i} & i = 0, 1 \end{matrix}

where, by convention, max(u, ⊥) = u.

Remark If we use min to replace max in the definition of summation, we get Moller and Tofts’ strong summation [MT90]. □

Clearly the summation operation is well defined. Moreover we have the following theorem.

Theorem 2.2.4 + : T s × T s ⟶ T s is continuous with respect to ⊑.

Proof: We only need to show that + is both left and right continuous. By symmetry, it is enough to check that + is left continuous.

Clearly + is left monotonic, i.e. for any T, T′ and T′′ of Ts, T ⊑ T′ implies T + T′′ ⊑ T′ + T′′. For every ω-chain T_{1}, ⋯, T_{n}, ⋯ and a T of Ts, we need to show that for every (V′, E′, r′, l′, t′) ∈ ⊔_{i∈ω}T_{i} + T, there is a (V′′, E′′, r′′, l′′, t′′) ∈ ⊔_{i∈ω}(T_{i} + T) such that V′ ⊆ V′′, E′ ⊆ E′′, r′ = r′′, l′ = l′′|_{E′} and t′ ⊑ t′′|_{V′}. Suppose (V′, E′, r′, l′, t′) ∈ ⊔_{i∈ω}T_{i} + T. Let v ∈ V′, then v ∈ V or there is a k such that for all i ≥ k we have v ∈ V_{i}. So there is a V′′ such that v ∈ V′′ and thus V′ ⊆ V′′, where V′′ is the set of vertices of a timed labelled tree of ⊔_{i∈ω}(T_{i} + T). In the same way we have E′′, r′′, l′′ and t′′, where E′ ⊆ E′′, r′ = r′′, l′ = l′′|_{E′} and t′ ⊑ t′′|_{V′}, such that (V′′, E′′, r′′, l′′, t′′) is a timed labelled tree of ⊔_{i∈ω}(T_{i} + T). □

2.2.4 Restriction

The restriction of a specific action λ ∈ A, where λ ≠ τ, on a timed synchronisation tree T represents a new timed synchronisation tree resulted by pruning away all edges labelled by λ and \overline{λ} together with their successors.

Definition 2.2.5 Let T be a timed synchronisation tree, possibly with parameters, and λ ∈ A, where λ ≠ τ, T \λ represents a new timed synchronisation tree T′, where

• V′ = {v : there is a path e_{1}, ⋯, e_{n} from the root r to v such that for any i = 1, ⋯, n, l(e_{i}) ≠ λ and l(e_{i}) ≠ λ̄} Chapter 2. Timed Synchronisation Trees 32 • E′ = E ∩ V′ × V′

• r′ = r

• l′ = l|_{E′}

• t′ = t|_{V′} Clearly the restriction operator is well defined. Moreover we have the following

theorem. Theorem 2.2.6 \λ : T s ⟶ T s is continuous with respect to ⊑. Proof: Similar to that of Theorem 2.2.2. □

Notation δ =^{def} (a({0})(λx.Ω))\a

δ may be described diagrammatically as:

• 0

2.2.5 Parallel

We can define the parallel operation on timed synchronisation trees. Figure 2–6 and Figure 2–7 show the result of the parallel operation of two timed synchronisation trees. Definition 2.2.7 For any T_{0}, T_{1} ∈ T s, the interleaving I(T_{0}, T_{1}) of their vertices is defined as

I(T_{0}, T_{1}) = {v : i = 0, 1&π_{i}(v) ∈ P(T_{i}) & v ∈ C^{∗}}

Chapter 2. Timed Synchronisation Trees 33

[figure: 3; a; u_{2} = 4^{1≤u_{1}≤3}; b; u_{3} = ∞^{3≤u_{2}≤4}^{1≤u_{1}≤3}; 5; ā; u_{2} = ∞^{2≤u_{1}≤5}]

Figure 2–6: Timed Synchronisation Trees T_{1} and T_{2}

[figure: u_{4} = ∞^{3≤u_{3}≤4}^{1 ˙−u_{1}≤u_{2}≤3−u_{1}}^{2≤u_{1}≤3}; b; u_{3} = 4^{1 ˙−u_{1}≤u_{2}≤3−u_{1}}^{2≤u_{1}≤3}; a; u_{2} = 3 − u_{1}^{2≤u_{1}≤3}; ā; 3; τ; u_{2} = 4^{2≤u_{1}≤3}; b; u_{3} = ∞^{3≤u_{2}≤4}^{2≤u_{1}≤3}; a; u_{2} = min(5 − t_{1}, 4)^{1≤u_{1}≤3}; ā; u_{3} = 4 − u_{2}^{2 ˙−u_{1}≤u_{2}≤min(5−u_{1},4)}^{1≤u_{1}≤3}; b; u_{4} = ∞^{3 ˙−u_{2}≤u_{3}≤4−u_{2}}^{2 ˙−u_{1}≤u_{2}≤min(5−u_{1},4)}^{1≤u_{1}≤3}; b; u_{3} = 5 − u_{1} − u_{2}^{3≤u_{2}≤min(5−u_{1},4)}^{1≤u_{1}≤3}; ā; u_{4} = ∞^{2 ˙−u_{1} ˙−u_{2}≤u_{3}≤5 ˙−u_{1} ˙−u_{2}}^{3≤u_{2}≤min(5−u_{1},4)}^{1≤u_{1}≤3}]

Figure 2–7: Parallel Composition of T_{1} and T_{2} where C = E_{0} ⊎ E_{1} ⊎ \{(e, e′) : e ∈ E_{0} & e′ ∈ E_{1} & \overline{l_{0}(e)} = l_{1}(e′) ≠ τ\}, P(T) is the set of all path starting from the root in T and we first define π_{i} : C ⟶ E_{i}, i = 0, 1, as

π_{i} = λ(x, j). \{ \begin{matrix}⟨⟩ & i ≠ j&j = 0, 1 \\ ⟨x⟩ & i = j \\ ⟨x_{i}⟩ & j = 2&x = (x_{0}, x_{1}) \end{matrix}

then we generalize π_{i} : C^{∗} ⟶ E_{i}^{∗} as follows

π_{i}(⟨e_{1} ⋯e_{n}⟩) = π_{i}(e_{1}) ⋯π_{i}(e_{n})

Clearly, for any timed synchronisation trees T_{1} and T_{2}, the interleaving I(T_{1}, T_{2}) of their vertices contains the null sequence ⟨⟩ and is closed under the initial subsequence relation.

Definition 2.2.8 For any T_{0}, T_{1} ∈ T s, their parallel composition T_{0} | T_{1} represents a new timed synchronisation tree T, where

• V = I(T_{0}, T_{1})

• E = {⟨v, v′⟩ : v, v′ ∈ V & ∃α ∈ C.v⟨α⟩ = v′}

• r = ⟨⟩

• l = λe. \{ \begin{matrix}l_{i}(α) & e = ⟨v, v′⟩ & v⟨α⟩ = v′ & α ∈ E_{i} & i = 0, 1 \\ τ & e = ⟨v, v′⟩ & v⟨α⟩ = v′ & α ∈ E_{0} × E_{1} \end{matrix}

• t = λv.S where if t_{i}(π_{i}(v)) = ⊥ (i = 0, 1) then S = ⊥; otherwise, let v = ⟨α_{1}, ⋯, α_{n}⟩, then S is the least set which satisfies

(1) (u_{1}, ⋯, u_{n}, u) ∈ S implies that

( ∑_{1≤j≤k_{1}} u_{j}, ⋯, ∑_{k_{l−1}<j≤k_{l}} u_{j}, u′) ∈ t_{0}(π_{0}(v))

( ∑_{1≤j≤k′_{1}} u_{j}, ⋯, ∑_{k′_{m−1}<j≤k′_{m}} u_{j}, u′′) ∈ t_{1}(π_{1}(v))

and

u = min(u′ − ∑_{k_{l}<j≤n} u_{j}, u′′ − ∑_{k′_{m}<j≤n} u_{j})

for some u′, u′′ ∈ D^{0}, where {k_{1}, ⋯, k_{l}} and {k′_{1}, ⋯, k′_{m}} (k_{1} ≤ ⋯ ≤ k_{l} and k′_{1} ≤ ⋯ ≤ k′_{m}) satisfy that ∀j ∈ {k_{1}, ⋯, k_{l}}. π_{0}(α_{j}) ≠ ⟨⟩ & ∀i ∈ {1, ⋯, n}−{k_{1}, ⋯, k_{l}}.π_{0}(α_{i}) = ⟨⟩ and ∀j ∈ {k′_{1}, ⋯, k′_{m}}.π_{1}(α_{j}) ≠ ⟨⟩&∀i ∈ {1, ⋯, n} − {k′_{1}, ⋯, k′_{m}}. π_{1}(α_{i}) = ⟨⟩; and

(2) (u′_{1}, ⋯, u′_{l}, u′) ∈ t_{0}(π_{0}(v)) and (u′′_{1}, ⋯, u′′_{m}, u′′) ∈ t_{1}(π_{1}(v)) implies that there are (u_{1}, ⋯, u_{n}, u) ∈ t(v), where n = l + m, such that

u′_{1} = ∑_{1≤j≤k_{1}} u_{j}, ⋯, u′_{l} = ∑_{k_{l−1}<j≤k_{l}} u_{j}

u′′_{1} = ∑_{1≤j≤k′_{1}} u_{j}, ⋯, u′′_{l} = ∑_{k′_{m−1}<j≤k′_{m}} u_{j}

and

u = min(u′ − ∑_{k_{l}<j≤n} u_{j}, u′′ − ∑_{k′_{m}<j≤n} u_{j})

where k_{1}, ⋯, k_{l}, k′_{1}, ⋯, k′_{m} are defined as in (1).

It is easy to see that the parallel operation is well defined. Moreover we have the following theorem.

Theorem 2.2.9 | : T s × T s ⟶ T s is continuous with respect to ⊑.

Proof: Analogous to Theorem 2.2.4. □

To present an expansion theorem which show the interleaving characterization of parallel composition of timed synchronisation trees, we first introduce two notations.

Notation For every u ∈ T and [V, E, r, l, t] ∈ T s, the time prefix (u)[V, E, r, l, t] represents a timed synchronisation tree [V, E, r, l, t′] where

t′ = λv. \{ \begin{matrix}⊥ & t(v) = ⊥ \\ t(r) + u & v = r & t(r) ∈ T \\ \{(u_{1} + u, ⋯, u_{n+1}, u′) : (u_{1}, ⋯, u_{n+1}, u′) ∈ t(v)\} & otherwise \end{matrix}

□

Intuitively, the time prefix (u)[V, E, r, l, t] represents the machine which, after a delay of time u, has the same behaviour as the machine represented by [V, E, r, l, t].

Notation For every u ∈ T and [V, E, r, l, t] ∈ T s, the time shift u >> [V, E, r, l, t] represents a timed synchronisation tree [V, E, r, l, t′] where

t′ = λv. \{ \begin{matrix}⊥ & t(v) = ⊥ \\ u′ ˙−u & v = r & t(r) = u′ \\ \{(u_{1} − u, ⋯, u_{n+1}, u′) : (u_{1}, ⋯, u_{n+1}, u′) ∈ t(v) & u_{1} ≥ u\} \\ otherwise \end{matrix}

□

Intuitively, the time shift u >> [V, E, r, l, t] represents the result of machine [V, E, r, l, t] after a delay of time u without any action.

Theorem 2.2.10 (Expansion Theorem) Let

T = ∑_{i∈I} a_{i}(S_{i})(λx_{i}.T_{i}) + (u)δ

and

T′ = ∑_{j∈J} b_{j}(S′_{j})(λy_{j}.T′_{j}) + (u′)δ

where Sup(S_{i}) ≤ u, Sup(S′_{j}) ≤ u′ for any i ∈ I and j ∈ J, then

T | T′ =

∑_{i∈I} a_{i}(S_{i} ∩ {w : w ≤ u′})(λz_{i}.(T_{i}{z_{i}/x_{i}} | z_{i} >> T′))

+

∑_{j∈J} b_{j}(S′_{j} ∩ {w : w ≤ u})(λz′_{j}.(z′_{j} >> T | T′_{j}{z′_{j}/y_{j}}))

+

∑_{j∈J^{i∈I}} τ(S_{i} ∩ S′_{j})(λz′′_{ij}.(T_{i}{z′′_{ij}/x_{i}} | T′_{j}{z′′_{ij}/y_{j}}))

+

min(u, u′)δ

where for any i ∈ I and j ∈ J, z_{i}, z′_{j} and z′′_{ij} are fresh parameters.

Proof: Let T_{l} = [V_{l}, E_{l}, r_{l}, l_{l}, t_{l}] and T_{r} = [V_{r}, E_{r}, r_{r}, l_{r}, t_{r}] represent the left hand side and right hand side of the expansion theorem, respectively. Clearly v ∈ V_{l} ⇔ π_{0}(v) ∈ P(T) & π_{1}(v) ∈ P(T′)

⇔ v = \{ \begin{matrix}⟨⟩ & or \\ ⟨(r, r_{i})⟩v′ & i ∈ I & π_{0}(v′) ∈ P(T_{i}) & π_{1}(v′) ∈ P(T′) \\ & & l(r, r_{i}) = a_{i}, or \\ ⟨(r′, r′_{j})⟩v′ & j ∈ J & π_{0}(v′) ∈ P(T) & π_{1}(v′) ∈ P(T′_{j}) \\ & & l(r′, r′_{j}) = b_{j}, or \\ ⟨((r, r_{i}), (r′, r′_{j}))⟩v′ & i ∈ I & j ∈ J & π_{0}(v′) ∈ P(T) & π_{1}(v′) ∈ P(T′_{j}) \\ & & l(r, r_{i}) = a_{i} = b̄_{j} = \overline{l(r′, r′_{j})} ≠ τ. \end{matrix}

This gives us a bijection f : V_{l} ⟶ V_{r} which satisfies f(r_{l}) = r_{r} and v→^{a}_{T_{l}}v′ implies f(v)→^{a}_{T_{r}}f(v′). Now we only need to show that for every v ∈ V_{l}, t_{l}(v) = t_{r}(f(v)) which follows from Definition 2.2.8. □

2.2.6 Relabelling

By relabelling a tree T with a relabelling function R : A ⟶ A we get a new tree which is resulted from T by changing the labels of the edges of T using the relabelling function R.

Definition 2.2.11 Let [V, E, r, l, t] ∈ T s and R : A ⟶ A be a relabelling function, [V, E, r, l, t][R] represents a new tree [V, E, r, l ∘ R, t].

It is easy to check that relabelling operation is well defined. Moreover we have the following theorem.

Theorem 2.2.12 [R] : T s ⟶ T s is continuous with respect to ⊑.

Proof: Analogous to Theorem 2.2.2. □

2.3 An Equivalence over Ts

Trees are concrete structures and contain detailed information. They distinguish too many things. For example, a tree T in general is not equal to a tree T + T, although it is hard to imagine any programming contexts in which their behaviour could be distinguished. In this section, we define an equivalence on Ts based on a notion of behaviour of timed synchronisation trees. The equivalence identifies those trees which have the same behaviour.

Definition 2.3.1 Given T, T′ ∈ T s, we write T ⟶^{a}_{u}T′, where a ∈ A and u ∈ T ,

whenever r→^{a}_{T} r′, u ∈ {u′ : (u′, u′′) ∈ t(r′)} and

(1) V′ = {v : there is a path from r′ to v in graph (V, E − {⟨r, r′⟩})}

(2) E′ = E ∩ V′ × V′

(3) l′ = l|_{E′}

(4) t′ = λv. \{ \begin{matrix}⊥ & t(v) = ⊥ \\ \{(u_{2}, ⋯, u_{n+1}, u′) : (u, u_{2}, ⋯, u_{n+1}, u′) ∈ t(v)\} & otherwise \end{matrix}

[figure: T_{u}; -; u : S; a; Sup(S)]

Figure 2–8: a timed synchronisation tree: T

[figure: T; T {u/x}; -; u : S; a; Sup(S)]

Figure 2–9: prefix operation

We can understand T ⟶^{a}_{u}T′ as that the machine represented by T performs an action a at time u and after doing so it evolves to a state represented by T′.

For convenience, we use Figure 2–8 to represent a timed synchronisation tree T, where T ⟶_{u}^{a} T_{u} for every u ∈ S. As a result, the procedure of prefixing a timed synchronisation tree, possibly with a parameter x, by a specific action a ∈ A and an interval S of T , can be described diagrammatically as in Figure 2–9.

We say a timed synchronisation tree is closed if it contains no open vertices. The presence of an open vertex in a timed synchronisation tree indicates that the tree is not fully defined.

Lemma 2.3.2 (1) If a(S)(λx.T) is a closed timed synchronisation tree and u ∈ S, then

a(S)(λx.T)⟶^{a}_{u}T {u/x}

(2) If T ⟶^{a}_{u}T′′, then T + T′⟶^{a}_{u}T′′ and T′ + T ⟶^{a}_{u}T′′.

Proof: Straightforward. □

Definition 2.3.3 A binary relation R over closed timed synchronisation trees is a tree bisimulation if (T_{1}, T_{2}) ∈ R implies that for any a ∈ A and u ∈ T ,

(1) if T_{1}⟶^{a}_{u}T′_{1}, then T_{2}⟶^{a}_{u}T′_{2} and (T′_{1}, T′_{2}) ∈ R for some T′_{2};

(2) if T_{2}⟶^{a}_{u}T′_{2}, then T_{1}⟶^{a}_{u}T′_{1} and (T′_{1}, T′_{2}) ∈ R for some T′_{1}; and

(3) t_{1}(r_{1}) = t_{2}(r_{2}).

We say two closed trees T and T′ are equivalent, written as T ≃ T′, if there is a tree bisimulation R such that (T, T′) ∈ R.

Definition 2.3.4 ≃ = ⋃{R : R is a tree bisimulation}

Proposition 2.3.5 ≃ is the largest tree bisimulation. Moreover it is an equivalence relation.

Proof: The result follows from the facts that the union, composition and inverse of tree bisimulations are still tree bisimulations. Also the identity relation over closed timed synchronisation trees is a tree bisimulation. □

Since (T s, ⊑) is a CPO and all operations are continuous with respect to ⊑, we may define infinite timed synchronisation trees along the standard line. For example, the infinite timed synchronisation tree μX.T represents the limit of the ω-chain T^{(0)}, ⋯, T^{(n+1)}, ⋯ where

T^{(0)} = Ω and T^{(n+1)} = T {T^{(n)}/X} Lemma 2.3.6 Given timed synchronisation trees T_{1} and T_{2}, if T_{1} ⊑ T_{2} and

T_{1}⟶^{a}_{u}T′_{1}, then T_{2}⟶^{a}_{u}T′_{2} and T′_{1} ⊑ T′_{2} for some tree T′_{2}.

Proof: The result follows from Definition 2.3.1. □

With Lemma 2.3.6, we can now define behaviours of an infinite timed synchronisation tree.

Definition 2.3.7 For an infinite tree μX.T, we say μX.T ⟶^{a}_{u}T′ if there is a n ∈ ω such that for any i ≥ n

T^{(i)}⟶^{a}_{u}T′_{i} and T′ = ⊔_{i≥n^{i∈ω}}T′_{i}

where T^{(0)} = Ω and T^{(i+1)} = T {T^{(i)}/X} for every i ∈ ω.

Proposition 2.3.8 μX.T ⟶^{a}_{u}T′ if and only if T {μX.T/X}⟶^{a}_{u}T′

Proof: Clearly T {μX.T/X} represents the limit of the ω-chain T^{1}, ⋯, T^{n}, ⋯, where

T^{1} = T {Ω/X} and T^{n+1} = T {T^{n}/X}

The result follows from the definition of the behaviour of infinite timed synchronisation trees. □

2.4 Conclusion

In this chapter, we presented a simple interleaving model, Timed Synchronisation Trees, for parallel computation in real-time systems. To represent machines which are only partially defined, we follow Hennessy [Hen85] and introduce a notion of open vertices. The presence of open vertices allows us to consider the model, timed synchronisation trees, as a CPO. All operations on timed synchronisation trees are continuous with respect to the CPO. This allows us to define infinite timed synchronisation trees along the standard lines.

Timed synchronisation trees may be used to give denotational semantics for a wide range of timed calculi, including Baeten and Bergstra’s Real Time Process Algebra and Moller and Tofts’ TCCS. In chapter 3, we will give a denotational semantics for Timed CCS based on timed synchronisation trees.

Timed CCS: A Timed Calculus of Communicating Systems

In this chapter, a formal description of Timed CCS (its syntax and semantics) is presented, together with some informal interpretations and remarks on design decisions.

3.1 Syntax

Timed CCS is an extension of Milner’s CCS [Mil80,Mil89a] with time. To define Timed CCS, we presuppose a countable set of names Λ, ranged over by a, b, of atomic actions not containing τ and ϵ. Let Act = Λ ∪ {τ}, ranged over by α, β. As in CCS, Λ can be partitioned into Γ, the set of names, and \overline{Γ} = \{ā |a ∈ Γ\}, the set of co-names, with the provision that ¯ ā = a. Actions a and ā are called complementary actions which form the basis of communications in our language, analogous to CCS. We also presuppose an infinite set V_{t} of time variables, ranged over by t, s, r. Let the time domain be (T ∪ {∞}, ≤), where T contains the least element 0 to represent the starting time and ≤ is a linear order over T . Note that we make no assumption about the underlying nature of time, allowing T , for example, to be (the set of natural numbers), ^{≥0} (the set of non-negative rationals) or ^{≥0} (the set of non-negative reals). We introduce ∞ to represent infinite time, where ∞ ∉ T . Our time expressions, ranged over by e, f, g, are defined as follows:

Definition 3.1.1

1 For any u ∈ T and t ∈ V_{t}, u and t are time expressions.

2 For every u ∈ T and time expression e, u × e is a time expression.

3 If e and f are time expressions, then e + f, e ˙−f, max(e, f) and min(e, f) are all time expressions, where e ˙−f represents the conditional expression if e < f then 0 else (e − f).

By convention, for any time expression e, we have e ≤ ∞, ∞ ∘ e = ∞, max(e, ∞) = ∞ and min(e, ∞) = e, where ∘ is + or ˙−. We will write e′ − e in place of e′ ˙−e whenever e ≤ e′.

Remark The decidability result of Chapter 5 will justify our decisions in the choice of time expressions. □

We also presuppose an infinite set V_{p} of process variables, ranged over by X, Y. The process expressions of Timed CCS, ranged over by E, F, are defined by the following BNF expression:

E ::= X |nil |α(t)_{e}^{e′}. E |E + F |E | F |E\a |E[S] |μX.E

where S : Act ⟶ Act is a relabelling function which satisfies \overline{S(a)} = S(ā) and S(τ) = τ, e and e′ are time expressions or e′ is the infinite time ∞.

Let E represent the set of all processes. Process nil cannot do any action, but idles any time. Prefix α(t)_{e}^{e′}. E represents the process which performs action α between time e and e′ (inclusive), where e and e′ are called the lower bound and upper bound of action α, respectively. Note that we only allow the upper bound to be the infinite time ∞ and therefore α(t)_{∞}^{e} . nil is not a process. Any occurrences of time variable t in E refer to the happening time of action α. After α happens, it evolves to a process E{u/t}, where u is the time at which α happens and E{u/t} is the result of substituting all free occurrence of t by u in E. Time variables in the language allow us to describe the notion of time dependency. For example, in the prefix α(t)_{e}^{e′}. E, the behaviours of process E depend on the happening time of action α whenever t is a free time variable of E. Summation E + F represents choice between processes E and F. The choice is made at the time of the first action of E or F, or at the time when only one process can idle (in this case the process which cannot delay is dropped from the future computation). Clearly the choice is deterministic with respect to time proceeding. Process E | F represents the parallel composition of processes E and F. Each of them may perform actions independently, or they may synchronise on complementary actions which represent communications between them, analogous to CCS. Parallel composition is synchronous with respect to time proceeding, i.e. the parallel composition E | F of the processes E and F can delay time u only when both E and F can.

There are two kinds of variables, time variables and process variables. The prefix operator α(t)_{e}^{e′} in α(t)_{e}^{e′}. E binds all free occurrences of time variable t in E and the recursive operator μX in μX.E binds all free occurrences of process variable X in E. These give, in the usual sense, the notions of free and bound occurrences of time and process variables. We use fv_{t}(E) and fv_{p}(E) to represent the set of all free time and process variables, respectively, occurring in E. We identify those process expressions which are the same up to changes of bound time and process variables. We say a process expression E is closed with respect to time variables (or process variables) if there is no free occurrences of time variables (or process variables) in E, i.e. fv_{t}(E) = ∅ (or fv_{p}(E) = ∅). An agent is a process expression which is closed with respect to both time and process variables. Let P represent the set of agents which is ranged over by P, Q, R. We occasionally allow multiple fixpoints of the form μX⃗.E⃗.

We say a process E is weakly guarded if every process variable of E is weakly guarded in E, where X is weakly guarded in E if every occurrence of X is in some subterm of form α(t)_{e}^{e′}. F of E. For example, the process a(t)_{0}^{∞}. X + b(s)_{1}^{10}. nil is weakly guarded. However the process a(t)_{2}^{10}. X + X is not weakly guarded as the second occurrence of X is not guarded in it.

Notation For convenience, we will write α.(E\{0/t\}) in place of α(t)_{0}^{0}. E and \underline{α}.E in place of α(t)_{0}^{∞}. E whenever t ∉ fv_{t}(E). □

We will also regard infinite time ∞ as a time expression when it is not important to distinguish between a time expression and the infinite time ∞.

Remark For simplicity, we only consider closed intervals in Timed CCS, i.e. in prefix α(t)_{e}^{e′}. E the action α can happen at any time of the closed interval e ≤ t ≤ e′. However, it is easy to extend Timed CCS to also deal with open intervals when their least upper bounds exist. As an example, we may use four prefixes α(t)_{>e}^{<e′}. E, α(t)_{≥e}^{<e′}. E, α(t)_{>e}^{≤e′}. E and α(t)_{≥e}^{≤e′}. E to replace the present one. □

As in [Mil89a], we introduce a notion of sort which is needed in the definition of a duration control operator. We say a process E has a sort L (L ⊆ Act), or L is a sort of E, written E : L, if the actions of E and all its derivatives lie in L ∪ {τ}. As for CCS, there is a natural way to assign a sort L(E) to each process E of Timed CCS.

Definition 3.1.2 Given sort L(X) for every process variable X, the syntactic sort L(E) of process E is inductively defined as follows:

1 L(τ(t)_{e}^{e′}. E) = L(E)

Chapter 3. Timed CCS: A Timed Calculus of Communicating Systems 47 2 L(a(t)_{e}^{e′}. E) = {a} ∪ L(E) 3 L(E + F) = L(E) ∪ L(F) 4 L(E | F) = L(E) ∪ L(F) 5 L(E\a) = L(E) − {a, ā} 6 L(E[S]) = {S(a) : a ∈ L(E)} 7 L(μX.E) = L(E) where, for every recursively defined process μX.E, the inclusion L(E) ⊆ L(X) must hold.

It is easy to show that L(E) is a sort of process E, i.e. E : L(E) (see [Mil89a]).

3.2 Semantics

In this section, we consider an operational and a denotational semantics for Timed CCS.

3.2.1 Operational Semantics

In order to define an operational semantics for Timed CCS, we use the general notion of a labelled transition system

(S, {⟶^{t} : t ∈ T })

which consists of a set S of states, a set T of transition labels and a transition relation ⟶^{t} ⊆ S × S for each t ∈ T.

In the transition system of Timed CCS, we take S to be P, the set of agents, and T to be (Act ∪ {ϵ}) × T, the set of pairs of actions and times (recall that ϵ ∉ Act). For convenience, we will write P ⟶^{α}_{u}P′ in place of (P, P′) ∈ ⟶^{(α,u)}, where

α ∈ Act, and P ⟶_{u}P′ in place of (P, P′) ∈ ⟶^{(ϵ,u)}.

The understanding of transition P ⟶^{α}_{u}P′ is that agent P performs action α at time u and then evolves to P′. The transition P ⟶_{u}P′ means that agent P idles up to time u without any action and then evolves to P′. P {u/t} represents the result of substituting all free occurrences of t in P by u.

To define the transition rules, we first define Moller and Tofts’ maximal delay time of processes before any action [MT90]. Definition 3.2.1

\begin{matrix}(1) | X |_{T} = 0 & (5) | E | F |_{T} = min( | E |_{T} , | F |_{T}) \\ (2) | nil |_{T} = ∞ & (6) | E\a |_{T} = | E |_{T} \\ (3) | α(t)_{e}^{e′}. E |_{T} = e′ & (7) | E[S] |_{T} = | E |_{T} \\ (4) | E + F |_{T} = max( | E |_{T} , | F |_{T}) & (8) | μX.E |_{T} = | E\{μX.E/X\} |_{T} \end{matrix}

Note that the maximal delay time | E |_{T} of process E is well defined only when E is weakly guarded. Henceforth we make this assumption about recursive terms.

All transition rules of the language are presented in Table 3–1. The rules are presented in natural deduction style which are read as follows: if the transition or transitions above the inference line can be inferred, then we can infer the transition below the line. The operational semantics of the language is then given by the least transition relations ⟶^{α}_{u} and ⟶_{u}, where α ∈ Act and u ∈ T , defined in Table 3–1.

For convenience, we introduce a notation δ to represent a dead process.

Notation δ =^{def} (a(t)_{0}^{0}. nil)\a □

Chapter 3. Timed CCS: A Timed Calculus of Communicating Systems 49

\overline{α(t)_{v}^{v′}. E⟶^{α}_{u}E\{u/t\}} (v ≤ u ≤ v′)

\overline{α(t)_{v}^{v′}. E⟶_{u}α(t)_{v ˙−u}^{v′−u}. (E\{u + t/t\})} (u ≤ v′)

\overline{nil⟶_{u}nil}  \frac{P ⟶_{u}P′  Q⟶_{u}Q′}{P + Q⟶_{u}P′ + Q′}
\frac{P ⟶_{u}P′}{P + Q⟶_{u}P′}  ( | Q |_{T} < u)  \frac{Q⟶_{u}Q′}{P + Q⟶_{u}Q′}  ( | P |_{T} < u)
\frac{P ⟶^{α}_{u}P′}{P + Q⟶^{α}_{u}P′}  \frac{Q⟶^{α}_{u}Q′}{P + Q⟶^{α}_{u}Q′}
\frac{P ⟶_{u}P′  Q⟶_{u}Q′}{P | Q⟶_{u}P′ | Q′}  \frac{P ⟶^{a}_{u}P′  Q⟶^{ā}_{u}Q′}{P | Q⟶^{τ}_{u}P′ | Q′}
\frac{P ⟶^{α}_{u}P′  Q⟶_{u}Q′}{P | Q⟶^{α}_{u}P′ | Q′}  \frac{P ⟶_{u}P′  Q⟶^{α}_{u}Q′}{P | Q⟶^{α}_{u}P′ | Q′}
\frac{P ⟶_{u}P′}{P \a⟶_{u}P′\a}  \frac{P ⟶^{α}_{u}P′}{P \a⟶^{α}_{u}P′\a}  (α ≠ a ∧ α ≠ ā)
\frac{P ⟶_{u}P′}{P [S]⟶_{u}P′[S]}  \frac{P ⟶^{α}_{u}P′}{P [S]⟶^{S(α)}_{u}P′[S]}
\frac{E\{μX.E/X\}⟶_{u}P}{μX.E⟶_{u}P}  \frac{E\{μX.E/X\}⟶^{α}_{u}P}{μX.E⟶^{α}_{u}P}

Table 3–1: Operational Rules for Timed CCS Chapter 3. Timed CCS: A Timed Calculus of Communicating Systems 50

Intuitively, the dead process δ neither performs any action nor idles. Note that we are abusing notation as δ also represents a timed synchronisation tree, but the intended meaning of it will be clear from the context. Proposition 3.2.2 For any weakly guarded agent P and u ∈ T , P ⟶_{u}P′ for some P′ if and only if u ≤ | P |_{T}. Proof: (⇐) Suppose u ≤ | P |_{T}, where u ∈ T, we proceed by transition induction. Case 1 P ≡ nil, then | P |_{T} = ∞ and P ⟶_{u}P. Case 2 P ≡ α(t)_{v}^{w}. Q, then | P |_{T} = w and P ⟶_{u}α(t)_{v ˙−u}^{w−u}. (Q{t + u/t}). Case 3 P ≡ P_{1} + P_{2}, then | P |_{T} = max( | P_{1} |_{T} , | P_{2} |_{T}). Suppose | P_{1} |_{T} ≥

| P_{2} |_{T}. By induction, P_{1}⟶_{u}P′_{1} for some P′_{1}. If u ≤ | P_{2} |_{T}, then P_{2}⟶_{u}P′_{2} for some P′_{2} and P ⟶_{u}P′_{1} + P′_{2}. If | P_{2} |_{T} < u, then P ⟶_{u}P′_{1}. The case of

| P_{1} |_{T} ≤ | P_{2} |_{T} is similar.

Case 4 P ≡ P_{1} | P_{2}, P ≡ Q\a and P ≡ Q[S] are similar to case 3. Case 5 P ≡ μX.E, then | E{μX.E/X} |_{T} = | μX.E |_{T}. Since X is weakly

guarded in E, by induction E{μX.E/X}⟶_{u}P′ for some P′. Therefore

P ⟶_{u}P′.

(⇒) Suppose P ⟶_{u}P′, we proceed by induction on the depth of the inference P ⟶_{u}P′. Case 1 P ≡ nil, then | P |_{T} = ∞ and u ≤ ∞. Case 2 P ≡ α(t)_{v}^{w}. E, then u ≤ w and | P |_{T} = w.

Chapter 3. Timed CCS: A Timed Calculus of Communicating Systems 51 Case 3 P ≡ P_{1} + P_{2}, then P_{1}⟶_{u}P′_{1} and P_{2}⟶_{u}P′_{2} for some P′_{1} and P′_{2} such that

P′ ≡ P′_{1} +P′_{2}, or P_{1}⟶_{u}P′ and | P_{2} |_{T} < u, or P_{2}⟶_{u}P′ and | P_{1} |_{T} < u. If P_{1}⟶_{u}P′_{1} and P_{2}⟶_{u}P′_{2}, where P′ ≡ P′_{1} + P′_{2}, then by induction u ≤ | P′_{1} |_{T} and u ≤ | P′_{2} |_{T}. So u ≤ max( | P_{1} |_{T} , | P_{2} |_{T}) = | P |_{T}. All other cases are similar.

Case 4 P ≡ P_{1} | P_{2}, P ≡ Q\a and P ≡ Q[S] are similar to case 3. Case 5 P ≡ μX.E, then E{P/X}⟶_{u}P′. By induction, u ≤ | E{P/X} |_{T} =

| P |_{T}. □ Proposition 3.2.3 For any agent P, we have

(1) if P ⟶_{u}P′ and P ⟶_{u}P′′, then P′ ≡ P′′;

(2) if P ⟶_{u}P′ and P′⟶_{v}P′′, then P ⟶_{u+v}P′′;

(3) if P ⟶_{u}P′and P′⟶^{α}_{v}P′′, then P ⟶^{α}_{u+v}P′′; and

(4) if P ⟶^{α}_{u}P′, then P ⟶_{u}P′′ and P′′⟶^{α}_{0}P′ for some P′′.

Proof: All these properties may be proved by induction on the depth of the inference of the form P ⟶_{u}P′. We only consider (1), as all others are similar.

For (1), we proceed by induction on the depth of the inference of the form P ⟶_{u}P′. Suppose P ⟶_{u}P′ and P ⟶_{u}P′′ Case 1 P ≡ nil, then P′ ≡ nil ≡ P′′. Case 2 P ≡ α(t)_{v}^{v′}. Q, then u ≤ v′ and P′ ≡ α(t)_{v ˙−u}^{v′−u}. (Q{u + t/t}) ≡ P′′. Case 3 P ≡ P_{1}+P_{2}, then u ≤ max( | P_{1} |_{T} , | P_{2} |_{T}). If u ≤ min( | P_{1} |_{T} , | P_{2} |_{T}),

then P_{1}⟶_{u}P′_{1} and P_{2}⟶_{u}P′_{2} for some P′_{1}, P′_{2} such that P′ ≡ P′_{1} + P′_{2}, and P_{1}⟶_{u}P′′_{1} and P_{2}⟶_{u}P′′_{2} for some P′_{1}, P′_{2} such that P′′ ≡ P′′_{1}+P′′_{2}. By induction, we have P′_{1} ≡ P′′_{1} and P′_{2} ≡ P′′_{2}. So P′ ≡ P′′. If | P_{1} |_{T} < u ≤ | P_{2} |_{T} then P_{2}⟶_{u}P′ and P_{2}⟶_{u}P′′. By induction, we have P′ ≡ P′′. Similarly, if

| P_{2} |_{T} < u ≤ | P_{1} |_{T}, we have P′ ≡ P′′.

Case 4 P ≡ P_{1} | P_{2}, P ≡ Q\a or P ≡ Q[S] similar to case 3.

Case 5 P ≡ μX.E, then E{μX.E/X}⟶_{u}P′ and E{μX.E/X}⟶_{u}P′′. By induction, P′ ≡ P′′. □

(1) shows the property of time determinacy. (2) and (3) show the property of time continuity and (4) says that atomic actions are instantaneous.

3.2.2 Denotational Semantics

Since Ts can be consider as a CPO, we can use Ts to interpret Timed CCS. To deal with process variables, we introduce a notion of environments which are mappings from V_{p} to Ts. Let Env be the set of environments, ranged over by ρ. For any environment ρ, ρ{T/X} represents a new environment which differs from ρ only at X, where it is defined to be T. The denotational semantics is given by a mapping

M : P ⟶ (Env ⟶ T s)

which is defined by induction on processes.

Definition 3.2.4 For any process E ∈ P and environment ρ, the denotation of E with respect to ρ, written as M(E)ρ, is defined by induction on E as

(1) M(X)ρ = ρ(X)

(2) M(nil)ρ = (∞)δ

(3) M(a(t)_{e}^{e′}. E) = a({u : e ≤ u ≤ e′})(λt.M(E))

(4) M(E + F)ρ = M(E)ρ + M(F)ρ

(5) M(E | F)ρ = M(E)ρ | M(F)ρ

(6) M(E\b)ρ = (M(E)ρ)\b

(7) M(E[S])ρ = (M(E)ρ)[S]

(8) M(μX.E)ρ = μT.(M(E)ρ{T/X})

Note that, if E is an agent, then M(E) is a constant function from Env to Ts, which may be regarded as an element of Ts.

Theorem 3.2.5 If an agent P is weakly guarded, then M(P) contains no open vertices, i.e. M(P) is a closed timed synchronisation tree.

Proof: Suppose P is weakly guarded. We show by induction on P that M(P) contains no open vertices. Clearly, M(nil) contains no open vertices and prefix, summation, restriction, parallel and relabelling operations preserve the property of no open vertices. The only nontrivial case is when P is of the form μX.Q. In this case, we use the fact that M(P) = ⨆_{i∈ω} M(P^{(i)}), where P^{(0)} = Ω and P^{(i+1)} = Q{P^{(i)}/X}. Clearly, for any vertex v of depth less than i in P^{(i)}, v cannot be an open vertex. It follows by the construction of limits that M(P) contains no open vertices. □

Definition 3.2.6 For any weakly guarded agents P and Q, we say P ≃ Q if M(P) ≃ M(Q).

Lemma 3.2.7 For every weakly guarded agent P, t(r) = | P |_{T} where (V, E, r, l, t) ∈ M(P).

Proof: For every agent P, let (V, E, r, l, t) ∈ M(P). By transition induction, we have Case 1 P ≡ nil, then | nil |_{T} = ∞ and clearly t(r) = ∞.

Case 2 P ≡ α(t)_{e}^{e′}. Q, then | P |_{T} = e′ and t(r) = Sup({u : u ≤ e′}) = e′.

Case 3 P ≡ P_{1} + P_{2}, then | P |_{T} = max( | P_{1} |_{T} , | P_{2} |_{T}). Let (V_{i}, E_{i}, r_{i}, l_{i}, t_{i}) ∈ M(P_{i}) where i = 1, 2. By induction, we have t_{i}(r_{i}) = | P_{i} |_{T} and t(r) =

max(t_{1}(r_{1}), t_{2}(r_{2})).

Case 4 P ≡ μX.E. Since P is weakly guarded, we have t′(r′) = | E{nil/X} |_{T}, where (V′, E′, r′, l′, t′) ∈ M(E)ρ{δ/T } for any environment ρ. It follows by the construction of limits that t(r) = | P |_{T}, where (V, E, r, l, t) ∈ M(P).

All other cases are similar. □

Theorem 3.2.8 P ≃ Q implies | P |_{T} = | Q |_{T}.

Proof: The result follows from Lemma 3.2.7. □

3.3 Applications

In this section, we define some derived operators and give some examples to demonstrate the use of the calculus for the specification of real-time systems. The examples will deal with three important aspects of real-time systems: time out, duration control and time dependency.

3.3.1 Derived Operators

We will only consider those derived operators which will be used in the sequel.

Chapter 3. Timed CCS: A Timed Calculus of Communicating Systems 55 Time Prefix The first derived operator is the time prefix of [MT90]. Definition 3.3.1 For any time expression e and weakly guarded process E, the time prefix (e)E is defined inductively as follows:

- (e)nil = nil

- (e)(a(t)_{f}^{f′}. E) = a(t)_{f+e}^{f′+e}. (E{t − e/t}) where t ∉ fv(e)

- (e)(E + F) = (e)E + (e)F

- (e)(E | F) = (e)E | (e)F

- (e)(E\a) = ((e)E)\a

- (e)(E[S]) = ((e)E)[S]

- (e)(μX.E) = (e)(E{μX.E/X})

Intuitively, (e)E represents a process which, after a delay of time e, has the same behaviour as process E.

For the time prefix operator, we have the following derived transition relation

(u + v)P ⟶_{u}(v)P

and transition rules

\frac{P ⟶^{α}_{v}P′}{(u)P ⟶^{α}_{u+v}P′}  \frac{P ⟶_{v}P′}{(u)P ⟶_{u+v}P′}

Note that ∞ is not a time expression and therefore (∞)δ is not a process. For convenience, we allow ourselves to write (∞)δ as syntactically identical to the process nil in the sequel.

Chapter 3. Timed CCS: A Timed Calculus of Communicating Systems 56 Time Shift The second derived operator is time shift which is the relative version of that of [BB91]. Definition 3.3.2 For any time expression e and weakly guarded process E, the time shift e >> E is defined inductively as follows:

- e >> nil = nil

- e >> (α(t)_{f}^{f′}. E) = α(t)_{(f ˙−e)+(max(e,f′)−f′)}^{f′ ˙−e}. (E{e + t/t}) where t ∉ fv(e)

- e >> (E + F) = e >> E + e >> F

- e >> (E | F) = e >> E | e >> F

- e >> (E\a) = (e >> E)\a

- e >> (E[S]) = (e >> E)[S]

- e >> (μX.E) = e >> (E{μX.E/X})

Informally, for any process E, if e ≤ | E |_{T}, then e >> E represents a state of E after a delay of time e without any action. If e > | E |_{T}, then e >> E represents the dead process δ. Note the subtlety in the definition for e >> (α(t)_{f}^{f′}. E). It ensures that the lower bound (f ˙−e) + (max(e, f′) − f′) > 0 whenever e > f′.

For the time shift operator, we have the following derived transition rules

\frac{P ⟶_{u+v}P′}{u >> P ⟶_{v}P′}  \frac{P ⟶^{α}_{u+v}P′}{u >> P ⟶^{α}_{v}P′}

Duration Control

In real-time systems, one important aspect of time-critical behaviour is duration control, which says that a process is allowed to run for a certain length of time, after that the control is passed to another process.

Consider a process which may behave as process E within time e and from time e it will behave as process F. We use E U_{e}F to represent such a process.

Definition 3.3.3 For weakly guarded processes E and F, the duration control E U_{e}F is inductively defined as follows:

- nil U_{e}F = (e)F

- (α(t)_{f}^{f′}. E) U_{e}F = α(t)_{f}^{min(e,f′)}. (E U_{e−t}F) + (e)F

- (E + E′) U_{e}F = (E U_{e}F) + (E′ U_{e}F)

- (E | E′) U_{e}F = (E U_{e}F) | (E′ U_{e}nil)

- (E\a) U_{e}F = ((E U_{e}(F [λ/a]))\a)[a/λ] where λ is a fresh action for E and F

- (E[S]) U_{e}F = (E U_{e}(F [S′]))[S][S^{′−1}] where S′|_{L(F)} : L(F) ⟶ Λ − (L(E) ∪ L(F)) and S′ is a bijection

- (μX.E) U_{e}F = (E{μx.E/X}) U_{e}F

Remark For any finite subsets A and B of Λ, where we insist that Λ is countably infinite, there is a relabelling function S : Λ ⟶ Λ which is a bijection and the range of S|_{A} is Λ − B. Since Λ is countable, we can construct such a relabelling function S as follows: (1) for the ith element a of A, where i = 1, 2, ⋯, let S(a) be the ith element of Λ − B; (2) for the ith element a of Λ − B, where i ≤ n (n is the size of A), let S(a) be the ith element of A; (3) for the jth element a of Λ − B, where j > n, let S(a) be a; and (4) for every element b of B − A, let S(b) be b. □

For the duration control operator, we have the following derived transition rules

\frac{Q⟶^{α}_{v}Q′}{P U_{u}Q⟶^{α}_{u+v}Q′} \frac{Q⟶_{v}Q′}{P U_{u}Q⟶_{u+v}Q′} v > 0

and

\frac{P ⟶^{α}_{u}P′}{P U_{u+v}Q⟶^{α}_{u}P′ U_{v}Q}  \frac{P ⟶_{u}P′}{P U_{u+v}Q⟶_{u}P′ U_{v}Q}

Remark Process E U_{e}F, even if E is the dead process, will behave as process F after time e. For example, process δ U_{10}F has the same behaviour as process (10)F. To define a strong version of duration control operator such that process δ U_{10}F represents the dead process δ, not (10)F, we can introduce a condition operator [e = f]E which represents process E when condition e = f holds, otherwise it represents the dead process δ.

3.3.2 Examples

In this section, we consider three examples and show how to describe the notions of time out, duration control and time dependency in Timed CCS.

Alternating Bit Protocol (Time Out)

Consider a timed implementation of the Alternating Bit Protocol which consists of four parts: Sender, Receiver and two unreliable transition lines, Ack and Trans. The unreliable transition lines may lose (but not corrupt) messages. Messages and acknowledgements are sent tagged with bits 0 and 1 alternately. Let b̂ = 1 − b, where b = 0, 1.

Sender, after accepting a message from the environment, sends the message together with an attached bit b (we assume the first message is tagged with 0), where b = 0 or 1, along the line Trans. Then it waits for an appropriate acknowledgement within time D, where D is the time Sender will wait before assuming the message had been lost. If it receives a correct acknowledgement within time D, Sender becomes ready to accept the next message from the environment and then transmits it with a bit b̂. If it receives a wrong acknowledgement within time D, it retransmits the message after a delay of time Δ. If it does not receive any acknowledgement after a delay of time D, it retransmits the message.

Sender = Sender_{0}

Sender_{b} = \underline{accept}.(Δ) \overline{send_{b}}.(Δ) Sending_{b}

Sending_{b} = ackb̂(t)_{0}^{D}. (Δ) \overline{send_{b}}.(Δ) Sending_{b} + ack_{b}(t)_{0}^{D}. (Δ) Senderb̂ + (D) \overline{send_{b}}.(Δ) Sending_{b}

Receiver, which we assume starts in a state waiting for a message tagged with 0, delivers the message after it receives a correct message along the transition line Trans and then transmits its acknowledgement along another transition line Ack. After doing so, it waits for a new message within time D, where D is the time that Receiver will wait before assuming its acknowledgement had been lost. If it receives a new message within time D, it again evolves to a state of delivering a message. If it receives the old message within time D, then it retransmits the acknowledgement after a delay of time Δ. If it does not receive any message after a delay of time D, it retransmits the acknowledgement.

Receiver = \underline{tran_{0}}.(Δ) Deliver_{0}

Deliver_{b} = \overline{deliver}.(Δ) \overline{reply}_{b}.(Δ) Reply_{b} Reply_{b} = tran_{b}(t)_{0}^{D}. (Δ) \overline{reply_{b}}.(Δ) Reply_{b} +

tranb̂(t)_{0}^{D}. (Δ) Deliverb̂ + (D + Δ) \overline{reply}_{b}(Δ) Reply_{b}

Two unreliable transition lines Trans and Ack behave as buffers of capacity one, but they may lose messages. We suppose the transition time for both transition lines is D′.

T rans = \underline{send_{0}}.(Δ) (τ(s)_{0}^{D′}. (Δ) T rans + (D′) \overline{tran_{0}}.(Δ) T rans)

+ \underline{send_{1}}.(Δ) (τ(s)_{0}^{D′}. (Δ) T rans + (D′) \overline{tran_{1}}.(Δ) T rans)

Ack = \underline{reply_{0}}.(Δ) (τ(s)_{0}^{D′}. (Δ) Ack + (D′) \overline{ack_{0}}.(Δ) Ack)

+ \underline{reply_{1}}.(Δ) (τ(s)_{0}^{D′}. (Δ) Ack + (D′) \overline{ack_{1}}.(Δ) Ack)

Now we may define the protocol as

P rotocol = (Sender | Receiver | T rans | Ack)\L

where L = {send_{0}, send_{1}, tran_{0}, tran_{1}, ack_{0}, ack_{1}, reply_{0}, reply_{1}}.

Since the least time for Sender to receive a correct acknowledgement after sending a message to the transition line is 2D′ + 4Δ, where D′(>> Δ) is the transition delay of the transition lines, we should take the timeout D > 2D′ + 4Δ.

Login Procedure (Duration Control)

Consider a user who attempts to use computers in a computer centre through a terminal. After the terminal is connected to a system, the system waits for the user’s valid login response. If the user enters a valid response r within 2 minutes, then the login procedure passes the control to a process Q which formalizes the user’s task. If the user’s login response is invalid, the system returns and still waits for user’s valid response. After waiting for 2 minutes without any valid response, the system rejects the login request and the connection between the terminal and the system is broken.

LP = \underline{connect}.(Δ) (P | (\underline{b}.Q + \underline{a}.nil))\\{a, b\}

P = L U_{2} ā.LP

L = \underline{r}.(Δ) b̄.nil + \underline{ir}.(Δ)L

Radar Gun (Time Dependency)

People who live in Glasgow but work in Edinburgh always like to drive as fast as possible on M8 between Glasgow and Edinburgh. We suppose the distance between Glasgow and Edinburgh is 45 (miles) and the maximal speed of a car is 90 (mph). However traffic wardens try to stop and punish heavily those people who drive too fast. We assume the maximum speed which is allowed on M8 is 70 (mph). When people leave Glasgow, they drive at speed 90 (mph) until they find by using their radar detectors that traffic wardens are using radar guns to measure their cars’ speed. After noticing the policemen’s presence, they immediately change their speed to 70 (mph) to avoid punishment. When they pass the policemen, they immediately return to 90 (mph) and drive at that speed until the next appearances of policemen. If there are no police on their way, people only require half an hour to arrive in Edinburgh. Otherwise, it takes longer.

Car = \underline{depart}.((0.5)arrive.nil + gunfire(t)_{0}^{0.5}. \overline{pass}(s)_{0}^{70^{−1}(45−90t)}. Car′(45 − 90t − 70s))

Car′(x) = (90^{−1}x)arrive.nil + gunfire(t)_{0}^{90^{−1}x}. \overline{pass}(s)_{0}^{70^{−1}(x−90t)}. Car′(x − 90t − 70s)

P olice = \underline{\overline{gunfire}}.\underline{pass}.P olice

For every car which runs from Glasgow to Edinburgh, we are only interested in the time it leaves Glasgow and the time it arrives in Edinburgh. So we define the whole system as:

Sys = (Car|P olice)\{gunfire, pass}

3.4 Conclusion

In this chapter, we proposed a timed calculus, Timed CCS, which is an extension of Milner’s CCS with time. We made no assumptions about the underlying nature of time, allowing it to be discrete, such as the natural numbers, or dense, such as the rationals and the reals. We also made no assumption of the Maximal Progress Principle which says that a process cannot delay when it may perform some internal action. Timed CCS is an interleaving model for real-time systems. Time variables in Timed CCS allow us to express the notion of time dependency in real-time systems. We gave two semantics, an operational and a denotational semantics, for Timed CCS and will show in Chapter 4 that these two semantics coincide in a sense that the equivalence on Timed CCS induced by the operational semantics is the same as the equivalence induced by the denotational semantics. We also presented some examples to show the use of the calculus for the specification of real-time systems.

Recently there have been a number of attempts to introduce time in welldeveloped process algebras. These include extensions of Milner’s CCS with time [CAM90,HR90,MT90,Wan90,Wan91], extensions of Hoare’s CSP with time [RR88, DS89,Sch91] and extensions of ACP with time [BB91,Gro90,Sif90]. Among these works, there are many features in common. For example, most works suppose atomic actions take no time, i.e. actions are instantaneous. This assumption is essential if we are to use an interleaving model for real-time systems. Also many works insist that the progress of time is deterministic which can be expressed as:

for every agent P, P ⟶_{u}P′ and P ⟶_{u}P′′ implies P′ ≡ P′′.

However, some work such as [Gro90] believes that the progress of time is not deterministic and idling also forces a choice of behaviour.

Some work such as [CAM90,HR90,Wan91,RR88,DS89,Sch91] is based on the assumption of the Maximal Progress Principle. We do not believe the Maximal Progress Principle is a natural assumption, as the internal behaviour of a nondeterministic machine is uncontrollable. How can we force an invisible and uncontrollable event to occur immediately?

The work such as [HR90,Gro90,Sif90] only deals with discrete time. In fact all these works introduce a special action to represent one unit time. In general these works cannot express the notion of time dependency. For example, consider a machine M which can perform an action a followed by an action b. The action a can happen at any time and if a happens at time t, then the action b must happen within another t time. We can define the machine M in discrete Timed CCS as:

M =^{def} a(t)_{0}^{∞}. b(s)_{0}^{t}. nil

It is not clear how this machine M could be defined in these calculi.

In [MT90], Moller and Tofts also make no assumption of the underlying nature of time, but they only provide expansion laws for discrete time. Similarly it is not clear how to define the machine M in TCCS of [MT90].

There are two ways to deal with the time dependency property: one is to introduce an infinite choice operator and the other is to introduce time variables. The extension of the syntax to include an infinite choice operator is very convenient descriptively but the mathematical foundations are immediately more complicated.

As an example, if we allow an infinite sum in timed synchronisation trees, then a hard question of whether the construction is continuous arises immediately.

In [BB91], Baeten and Bergstra introduce a notion of integration which in fact is just a special form of infinite summation. ACP ρI is more general and complicated than Timed CCS. As pointed out by Klusener in [Klu91] that we do not know real-life processes which are ruled out by restricting to “prefixed integration” processes. However, if we restrict to those “prefixed integration” processes, the resulting language corresponds to Timed CCS.

In [Wan91], Wang also independently introduces time variables to fix a serious error in the expansion law of his early paper [Wan90] (the error was pointed out to Wang by the author of this thesis). The work of [Wan90,Wan91] is based on the assumption of the maximal progress principle and the ability of expressing the notion of time out is achieved by using the property that the internal action τ cannot delay. Due to the assumption of the Maximal Progress Principle, it is difficult to extend the work of [Wan90,Wan91] to deal with open intervals over dense time domains. As a consequence, we cannot express a notion of some action happening before a certain time or a time out happens for some action at that time by extending [Wan90,Wan91]. For example, we cannot define a machine P which is defined in a possible extension of Timed CCS as

P =^{def} a(t)_{≥0}^{<25}. nil + b(s)_{≥25}^{<∞}. nil

by extending [Wan90,Wan91]. This is a drawback, as an adequate description of time out becomes impossible.

Strong Equivalence

A more abstract semantics for Timed CCS is achieved by identifying those agents which cannot be distinguished by any external observation of their behaviour. The notion of bisimulation [Par81,Mil89a] is a standard device for defining behavioural equivalence for process algebras. In this chapter, we extend the notion of strong bisimulation of [Mil89a] to timed processes. Strong equivalence treats the internal action τ in the same way as all other actions and is a rather strict equivalence relation. However strong equivalence enjoys many nice properties. It is a congruence relation and many of the equational laws including an expansion law which we wish to use in practice are valid for it. It is decidable for finite processes (see Chapter 5) and there is a simple proof system (see Chapter 6) which is complete for finite processes over dense time domains.

4.1 Strong Bisimulation

We do not wish to distinguish agents which, in some sense, have the same behaviour. The notion of bisimulation between agents captures the idea of having the same behaviour. We say two agents are not equivalent if a distinction can be detected by an experimenter who interacts with each of them.

Chapter 4. Strong Equivalence 66 Definition 4.1.1 A binary relation R ⊆ P×P is a strong bisimulation if (P, Q) ∈ R implies that for any α ∈ Act and u ∈ T

(1) if P ⟶^{α}_{u}P′, then Q⟶^{α}_{u}Q′ and (P′, Q′) ∈ R for some Q′;

(2) if P ⟶_{u}P′, then Q⟶_{u}Q′ and (P′, Q′) ∈ R for some Q′;

(3) if Q⟶^{α}_{u}Q′, then P ⟶^{α}_{u}P′ and (P′, Q′) ∈ R for some P′; and

(4) if Q⟶_{u}Q′, then P ⟶_{u}P′ and (P′, Q′) ∈ R for some P′.

We say two agents P and Q are strongly bisimilar, denoted by P ∼ Q, if there is a strong bisimulation R such that (P, Q) ∈ R. Definition 4.1.2 ∼ = ⋃ {R : R is a strong bisimulation}. Proposition 4.1.3 ∼ is the largest strong bisimulation. Moreover, it is an equivalence relation. Proof: The proof follows from the facts that the union, composition and inverse of strong bisimulations are still strong bisimulations and also the identity over agents is a strong bisimulation. □ Lemma 4.1.4 For any agents P and Q, P ∼ Q implies |P |_{T} = |Q|_{T}. Proof: The result follows from Proposition 3.2.2. □ Definition 4.1.5 A binary relation R over P is a strong T -bisimulation if (P, Q) ∈ R implies that for any α ∈ Act and u ∈ T

(1) if P ⟶^{a}_{u}P′, then Q⟶^{a}_{u}Q′ and (P′, Q′) ∈ R for some Q′;

(2) if Q⟶^{a}_{u}Q′, then P ⟶^{a}_{u}P′ and (P′, Q′) ∈ R for some P′; and Chapter 4. Strong Equivalence 67 (3) |P |_{T} = |Q|_{T}.

Similarly to strong bisimulation, we say two agents P and Q are strong T - bisimilar, denoted by P ∼_{T} Q, if there is a strong T -bisimulation R such that (P, Q) ∈ R. Definition 4.1.6 ∼_{T} = ⋃ {R : R is a strong T −bisimulation}

“Bisimulation up to” of [Mil89a] is a useful technique for reducing the size of the relation needed to define a bisimulation. We generalize it to timed case and first define a notion of T -bisimulation up to ∼_{T}. Definition 4.1.7 We say S is a strong T -bisimulation up to ∼_{T} if P SQ implies that

(1) whenever P ⟶^{α}_{u}P′ then Q⟶^{α}_{u}Q′ and P′ ∼_{T} S ∼_{T} Q′ for some Q′;

(2) whenever Q⟶^{α}_{u}Q′ then P ⟶^{α}_{u}P′ and P′ ∼_{T} S ∼_{T} Q′ for some P′; and

(3) | P |_{T} = | Q |_{T}.

Similarly we can define a notion of strong bisimulation up to ∼. Definition 4.1.8 We say S is a strong bisimulation up to ∼ if P SQ implies that

(1) if P ⟶^{α}_{u}P′, then Q⟶^{α}_{u}Q′ and P′ ∼ S ∼ Q′ for some Q′;

(2) if P ⟶_{u}P′, then Q⟶_{u}Q′ and P′ ∼ S ∼ Q′ for some Q′;

(3) if Q⟶^{α}_{u}Q′, then P ⟶^{α}_{u}P′ and P′ ∼ S ∼ Q′ for some P′; and

(4) if Q⟶_{u}Q′, then P ⟶_{u}P′ and P′ ∼ S ∼ Q′ for some P′. Proposition 4.1.9 Chapter 4. Strong Equivalence 68 1 If S is a strong T -bisimulation up to ∼_{T}, then S ⊆∼_{T}. 2 If S is a strong bisimulation up to ∼, then S ⊆∼. Proof: Suppose S is a strong T -bisimulation (strong bisimulation) up to ∼_{T} (∼) . We only need to show that ∼_{T} S ∼_{T} (∼ S ∼) is a strong T -bisimulation (strong bisimulation), which is analogous to Lemma 4.3.5 of [Mil89a]. □

Hence, to prove P ∼_{T} Q (P ∼ Q), we only need to find a strong T -bisimulation (strong bisimulation) up to ∼_{T} (∼) which contains (P, Q). Lemma 4.1.10 For weakly guarded agent P, P ⟶_{u}P′ implies P′ ∼ u >> P. Proof: We proceed by induction on the depth of the inference of the form P ⟶_{u}P′. Suppose P ⟶_{u}P′. Case 1 P ≡ nil, then P′ ≡ nil ∼ u >> P. Case 2 P ≡ α(t)_{v}^{v′}. Q, then v ≤ u ≤ v′ and P′ ≡ α(t)_{v ˙−u}^{v′−u}. (Q{u + t/t}) ∼ u >> P. Case 3 P ≡ P_{1}+P_{2}, then u ≤ max( | P_{1} |_{T} , | P_{2} |_{T}). If u ≤ min( | P_{1} |_{T} , | P_{2} |_{T}),

then P_{1}⟶_{u}P′_{1}, P_{2}⟶_{u}P′_{2} and P′ ≡ P′_{1} + P′_{2}. By induction, we have P′_{1} ∼ u >> P_{1} and P′_{2} ∼ u >> P_{2}. Hence P′ ∼ u >> P. If | P_{1} |_{T} < u ≤ | P_{2} |_{T}, then P_{2}⟶_{u}P′. By induction, we have P′ ∼ u >> P_{2}. Since | P_{1} |_{T} < u, we have u >> P_{1} ∼ δ. Hence P′ ∼ u >> P. The case of | P_{2} |_{T} < u ≤ | P_{1} |_{T}

is similar to that of | P_{1} |_{T} < u ≤ | P_{2} |_{T}.

Case 4 P ≡ P_{1} | P_{2}, P ≡ Q\a or P ≡ Q[S], similar to case 3. Case 5 P ≡ μX.E, then E{μX.E/X}⟶_{u}P′. By induction,

P′ ∼ u >> E{μX.E/X} = u >> P

□

Due to the property of time determinacy, the equivalences ∼ and ∼_{T} coincide over weakly guarded agents. As the maximal delay time of a process is syntactically defined, it is easier to show a relation of strong T -bisimulation than that of strong bisimulation.

Proposition 4.1.11 For any weakly guarded agents P and Q, P ∼ Q if and only if P ∼_{T} Q.

Proof: For direction (⇒), it is enough to show that the relation

∼ ∩ {(P, Q) : P and Q are weakly guarded}

is a strong T -bisimulation. The result follows from the definitions of strong bisimulations and strong T -bisimulations.

For direction (⇐), we only need to show that

{(u >> P, u >> Q) : P ∼_{T} Q &u ≤ | P |_{T} & P and Q are weakly guarded}

is a strong bisimulation up to ∼. The result follows from Lemma 4.1.10 and Proposition 3.2.2. □

4.2 Operational Characterization of ≃

In Chapter 3, we gave an operational and a denotational semantics for Timed CCS. In this section, we show that the two semantics of Timed CCS coincide over weakly guarded agents, i.e. the equivalence ≃ and ∼ are identical over weakly guarded agents. This informally states that the model Ts differentiates two machines if and only if they can be differentiated by an experimenter.

Lemma 4.2.1 For any weakly guarded agent P, P ⟶^{α}_{u}P′ implies M(P)⟶^{α}_{u}M(P′).

Proof: See [Mil80]. □

Chapter 4. Strong Equivalence 70 Lemma 4.2.2 For any weakly guarded agent P, M(P)⟶^{α}_{u}T implies P ⟶^{α}_{u}P′ and M(P′) = T for some agent P′. Proof: See [Mil80]. □ Theorem 4.2.3 (Operational Characterization Theorem) For any weakly guarded agents P and Q, P ∼ Q if and only if P ≃ Q. Proof: (⇒) It is enough to show that

S = {(M(P), M(Q)) : P ∼ Q}

is a tree bisimulation.

(1) if M(P)⟶^{α}_{u}T, then P ⟶^{α}_{u}P′ and M(P′) = T. Since P ∼ Q, there is a Q′ such that Q⟶^{α}_{u}Q′ and P′ ∼ Q′. So M(Q)⟶^{α}_{u}T′ with M(Q′) = T′ and (M(P′), M(Q′)) ∈ S.

(2) if M(Q)⟶^{α}_{u}T, similar to (1).

(3) t(r) = | P |_{T} = | Q |_{T} = t′(r′), where (V, E, r, l, t) ∈ M(P) and (V′, E′, r′, l′, t′) ∈ M(Q).

(⇐) It is easy to check that the relation

S = {(P, Q) : P ≃ Q where P, Q weakly guarded}

is a strong T -bisimulation. □

4.3 Properties of Strong Equivalence

In this section, we present some properties for strong equivalence. The first five propositions are proved in a standard way by demonstrating appropriate strong bisimulations. Proposition 4.3.1 (Laws for Prefix) 1 α(t)_{u}^{u′}. E ∼ α(s)_{u}^{u′}. (E{s/t}) where s is free for t in E 2 α(t)_{u}^{u′}. E ∼ (u′)δ where u > u′ 3 α(t)_{u}^{u′}. E ∼ α(t)_{u}^{u′}. E + (u′)δ 4 α(t)_{u}^{v}. E + α(t)_{v}^{u′}. E ∼ α(t)_{u}^{u′}. E where u ≤ v ≤ u′

(1) shows that α-conversion preserves strong equivalence. From (2), we see that timing can also block actions. As an example, agent a(t)_{10}^{5}. nil cannot perform action a, but idles time 5 before it dies. Proposition 4.3.2 (Laws for Summation) 1 P + δ ∼ P 2 P + P ∼ P 3 P + Q ∼ Q + P 4 P + (Q + R) ∼ (P + Q) + R Proposition 4.3.3 (Laws for Restriction)

1 ((u)δ)\a ∼ (u)δ

2 (α(t)_{u}^{u′}. E)\a ∼ α(t)_{u}^{u′}. (E\a) where α ≠ a ∧ α ≠ ā

3 (α(t)_{u}^{u′}. E)\a ∼ (u′)δ where α = a ∨ α = ā

4 (P + Q)\a ∼ P \a + Q\a

The restriction operator is distributive over summation. We will see that for any finite agent P which does not contain parallel and relabelling operators, by using the above laws, we can find an agent P′, where P′ does not contain the restriction operator (except δ), such that P ∼ P′.

Proposition 4.3.4 (Laws for Relabelling)

1 ((u)δ)[S] ∼ (u)δ

2 (α(t)_{u}^{u′}. E)[S] ∼ (S(α))(t)_{u}^{u′}. (E[S])

3 (P + Q)[S] ∼ P [S] + Q[S]

The relabelling operator is also distributive over choice and we will see that for every finite agent P which does not contain the parallel operator, by using the above laws, we can find an agent P′, where P′ does not contain the relabelling operator, such that P ∼ P′.

Proposition 4.3.5 (Laws for Recursion) μX.E ∼ E{μX.E/X}

Until now, we have only defined strong equivalence over agents. However, we may also extend strong equivalence to processes along the standard lines.

Definition 4.3.6 For any processes E and F which are closed with respect to process variables and contain at most free time variables t⃗ = (t_{1}, …, t_{n}), we write E ∼ F if for any u⃗ ∈ T^{n} we have E{u⃗/t⃗} ∼ F {u⃗/t⃗}.

Definition 4.3.7 For any processes E and F which contain at most free process variables X⃗ = (X_{1}, …, X_{n}), we write E ∼ F if for any agents P⃗ = (P_{1}, …, P_{n}), we have E{P⃗ /X⃗} ∼ F {P⃗ /X⃗}.

It is easy to check that all of the above laws still hold for processes. Moreover, we have the following expansion law. To simplify the presentation, we introduce a notion of normal form.

Definition 4.3.8 A process E ≡ ∑_{i∈I} α_{i}(t_{i})_{e_{i}}^{e′_{i}}. E_{i} + (e)δ is in normal form if for any i ∈ I, e′_{i} ≤ e and E_{i} is also in normal form.

Clearly, for any normal form E ≡ ∑_{i∈I} α_{i}(t_{i})_{e_{i}}^{e′_{i}}. E_{i} + (e)δ, we have | E |_{T} = e.

Proposition 4.3.9 (Expansion Law) Given normal forms

E ≡ ∑_{i∈I} α_{i}(t_{i})_{e_{i}}^{e′_{i}}. E_{i} + (e)δ

and

F ≡ ∑_{j∈J} β_{j}(s_{j})_{f_{j}}^{f′_{j}}. F_{j} + (f)δ

we have

E | F ∼

∑_{i∈I} α_{i}(r_{i})_{e_{i}}^{min(e_{i},f)}. (E_{i}{r_{i}/t_{i}} | r_{i} >> F)

+

∑_{j∈J} β_{j}(r′_{j})_{f_{j}}^{min(f′_{j},e)}. (r′_{j} >> E | F_{j}{r′_{j}/s_{j}})

+

∑_{j∈J^{i∈I}^{α_{i}=β̄_{j}}} τ(r_{ij})_{max(e_{i},f_{j})}^{min(e′_{i},f′_{j})}. (E_{i}{r_{ij}/t_{i}} | F_{j}{r_{ij}/s_{j}})

+

(min(e, f))δ

where for any i ∈ I, j ∈ J, r_{i}, r′_{j} and r_{ij} are fresh time variables.

Proof: We only need to consider the case in which E and F are agents and show that a relation R, where R is the least relation satisfying

(1) ∼_{T} ⊆ R; and

(2) for any normal forms P ≡ ∑_{i∈I} α_{i}(t_{i})_{v_{i}}^{v′_{i}}. E_{i} + (v)δ and Q ≡ ∑_{j∈J} β_{j}(s_{j})_{w_{j}}^{w′_{j}}. F_{j} + (w)δ, let G be the right hand side of expansion law for P and Q, then (P | Q, G) ∈ R,

is a strong T -bisimulation up to ∼_{T}.

Suppose (S, S′) ∈ R. The case of S ∼_{T} S′ is trivial. Now suppose S ≡ P | Q, where P ≡ ∑_{i∈I} α_{i}(t_{i})_{v_{i}}^{v′_{i}}. E_{i} + (v)δ and Q ≡ ∑_{j∈J} β_{j}(s_{j})_{w_{j}}^{w′_{j}}. F_{j} + (w)δ are in normal form, and S′ ≡ G, where G is the right hand side of expansion law for P and Q. Clearly | P | Q |_{T} = min(v, w) = | G |_{T}.

Case 1 Suppose P | Q⟶^{α}_{u}R Case 1.1 P ⟶^{α}_{u}P′, Q⟶_{u}Q′ and R ≡ P′ | Q′, then for some i ∈ I and j ∈ J, α = α_{i}, v_{i} ≤ u ≤ min(v′_{i}, w) , P′ ≡ E_{i}{u/t_{i}} and Q′ ∼ u >> Q. So (by congruence property, which is demonstrated next) R ∼ E_{i}{u/t_{i}} | u >>

Q. Clearly G⟶^{α}_{u}(E_{i}{r_{i}/t_{i}} | r_{i} >> Q){u/r_{i}} and E_{i}{u/t_{i}} | u >> Q ∼

(E_{i}{r_{i}/t_{i}} | r_{i} >> Q){u/r_{i}}.

Case 1.2 P ⟶_{u}P′, Q⟶^{α}_{u}Q′ and R ≡ P′ | Q′. Similar to case 1.1.

Case 1.3 α = τ, P ⟶^{a}_{u}P′, Q⟶^{ā}_{u}Q′ and R ≡ P′ | Q′ for some a. Then α_{i} = a, β_{j} = ā, w_{j} ≤ u ≤ min(v′_{i}, w′_{j}), P′ ≡ E_{i}{u/t_{i}} and Q′ ≡ F_{j}{u/s_{j}}

for some i ∈ I, j ∈ J. Clearly, G⟶^{τ}_{u}(E_{i}{r_{ij}/t_{i}} | F_{j}{r_{ij}/s_{j}}){u/r_{ij}} and

E_{i}{u/t_{i}} | F_{j}{u/s_{j}} ∼ (E_{i}{r_{ij}/t_{i}} | F_{j}{r_{ij}/s_{j}}){u/r_{ij}}.

Case 2 Suppose G⟶^{α}_{u}R, similar to case 1. □

4.4 Strong Congruence

Strong equivalence is a congruence relation, i.e. it is substitutive under all operators including the recursive operator. This is shown by the following two propositions.

Proposition 4.4.1 For any processes E and F, E ∼ F implies

(1) α(t)_{e}^{e′}. E ∼ α(t)_{e}^{e′}. F  (4) E\a ∼ F \a
(2) E + G ∼ F + G  (5) E[S] ∼ F [S]
(3) E | G ∼ F | G

Proof: All these properties can be proved by exhibiting appropriate strong bisimulations. For example, for (3), it is enough to consider agents and show that

S = {(P | R, Q | R) : P ∼ Q}

is a strong bisimulation. □

In the sequel, we use E⃗ ∼ F⃗ to represent componentwise strong equivalences between E⃗ and F⃗.

Proposition 4.4.2 For any processes E⃗ and F⃗ which contain at most free process variables X⃗, E⃗ ∼ F⃗ implies μX⃗.E⃗ ∼ μX⃗.F⃗.

Proof: Analogous to Proposition 4.4.12 of [Mil89a]. □

For any finite process E, by using the laws for restriction, the laws for relabelling and the expansion law, we can find a process E′, where E′ does not contain the restriction operator (except δ), relabelling operator and parallel operator, such that E ∼ E′.

4.5 Unique Solution of Equations

In this section, we focus on the solutions of the equations X⃗ = E⃗. We will show that under certain conditions, the equations X⃗ = E⃗ have an unique solution up to strong equivalence.

Definition 4.5.1 We say the equations X⃗ = E⃗ are weakly guarded if all X⃗ are weakly guarded in E⃗.

The most important property of a weakly guarded process is that its first possible actions are completely independent of whatever we may substitute for its process variables.

Lemma 4.5.2 For any process E and agents P⃗, if process variables X⃗ are weakly guarded in E and E{P⃗ /X⃗}⟶^{α}_{u}P′ (or E{P⃗ /X⃗}⟶_{u}P′) , then P′ has the form E′{P⃗ /X⃗} for some process E′. Moreover, for any agents Q⃗, E{Q⃗/X⃗}⟶^{α}_{u}E′{Q⃗/X⃗} (or E{Q⃗/X⃗}⟶_{u}E′{Q⃗/X⃗}).

Proof: Analogous to Lemma 4.5.13 of [Mil89a]. □

Lemma 4.5.3 For any process E which contains at most free process variables X⃗ and every X_{i} ∈ X⃗ is weakly guarded in E, then for any agents P⃗ and Q⃗, | E{P⃗ /X⃗} |_{T} = | E{Q⃗/X⃗} |_{T}.

Proof: The result follows from Definition 3.2.1. □

For any weakly guarded equations X⃗ = E⃗, if they have solutions, then the solutions are unique up to strong equivalence.

Proposition 4.5.4 For any processes E_{i} (i ∈ I) which are closed with respect to time variables and contain at most free process variables X_{i} (i ∈ I), let all X_{i} (i ∈ I) be weakly guarded in each E_{j} (j ∈ I). Then

P⃗ ∼ E⃗{P⃗ /X⃗} and Q⃗ ∼ E⃗{Q⃗/X⃗} implies P⃗ ∼ Q⃗

Proof: Analogous to Proposition 4.5.14 of [Mil89a]. □

It is easy to see that any weakly guarded equations have solutions. Therefore any weakly guarded equations have an unique solution up to strong equivalence.

Corollary 4.5.5 (Unique Solution) For any weakly guarded equations X⃗ = E⃗, where E⃗ are closed with respect to time variables and contain at most free process variables X⃗, there is an unique solution P⃗ (up to strong equivalence) such that

P⃗ ∼ E⃗{P⃗ /X⃗}

4.6 Modal Characterization of ∼

In this section, we give an alternative characterization of strong equivalence based on a simple modal language. Our modal language is an extension of the well-known Hennessy-Milner Logic with time.

There are some works on introducing real-time explicitly to Hennessy-Milner Logic, possibly with recursion. Among others, we mention here the works of [CM92,HLW91,Mol90].

The formulas of the modal language are defined by the following BNF expression:

ψ = tt | ¬ψ | ψ_{1} ∧ ψ_{2} | ⟨α, v⟩ψ | ⟨u⟩ψ

where α ∈ Act, u, v ∈ T or v ≡ ∞. Let L be the set of all formulas defined by the above BNF expression, ranged over by ψ, φ.

The intended meaning of ⟨α, u⟩ψ is that there is an action α which happens not later than time u and after α happens the formula ψ will hold. Note that the above defined language is not a standard extension of Hennessy-Milner logic with time. The modal formula ⟨α, u⟩ψ allows action al to occur at ot before time u. The formula ⟨u⟩ψ means there is a possibility that after a delay of time u, ψ will hold.

The formulas of L are interpreted over transition systems of the form

(S, {⟶^{α}_{u} : α ∈ Act & u ∈ T } ∪ {⟶_{u} : u ∈ T })

where α ∈ Act, u ∈ T. As the operational semantics of Timed CCS is defined by a transition system of the above form, we can interpret the formulas of L over processes of Timed CCS.

Definition 4.6.1 We say a Timed CCS agent P satisfies a formula ψ ∈ L if P ⊧ ψ, where P ⊧ ψ is inductively defined as follows:

(1) P ⊧ tt

(2) P ⊧ ¬ψ if and only if ¬P ⊧ ψ

(3) P ⊧ ψ ∧ φ if and only if P ⊧ ψ ∧ P ⊧ φ

(4) P ⊧ ⟨α, u⟩ψ if and only if ∃v ∈ T ∃P′(v ≤ u ∧ P ⟶^{α}_{v}P′ ∧ P′ ⊧ ψ)

(5) P ⊧ ⟨u⟩ψ if and only if ∃P′(P ⟶_{u}P′ ∧ P′ ⊧ ψ)

The important derived operators are the duals of ⟨α, v⟩ and ⟨u⟩, denoted by [α, v] and [v], respectively.

[α, v]ψ =^{def} ¬⟨α, v⟩¬ψ

[u]ψ =^{def} ¬⟨u⟩¬ψ

Informally the formula [α, u]ψ means that ψ holds after every action α which happens before or at time u. The formula [u]ψ means that ψ holds after every delay of time u.

Further derived operators are:

ff =^{def} ¬tt

A ∨ B =^{def} ¬(¬A ∧ ¬B)

A → B =^{def} ¬A ∨ B

All these operators have the usual meanings.

Bisimilarity preserves modal properties of L, i.e. bisimilar agents of Timed CCS enjoy the same modal properties of L.

Theorem 4.6.2 P ∼ Q implies that for any formula ψ of L, P ⊧ ψ if and only if Q ⊧ ψ.

Proof: Suppose P ∼ Q. For any formula ψ of L, we prove P ⊧ ψ if and only if Q ⊧ ψ by induction on the structure of ψ. We only show modalities, the other parts are trivial.

(1) ψ ≡ ⟨α, u⟩φ, by symmetry we only need to show that P ⊧ ⟨α, u⟩φ implies Q ⊧ ⟨α, u⟩φ. Suppose P ⊧ ⟨α, u⟩φ, then we have P ⟶^{α}_{v}P′ for some P′ and v such that v ≤ u and P′ ⊧ φ. Since P ∼ Q, we have Q⟶^{α}_{v}Q′ for some Q′ such that P′ ∼ Q′. By induction, Q′ ⊧ φ. So Q ⊧ ⟨α, u⟩φ.

(2) ψ ≡ ⟨u⟩φ, similarly we only need to show that P ⊧ ⟨u⟩φ implies Q ⊧ ⟨u⟩φ. Suppose P ⊧ ⟨u⟩φ, then P ⟶_{u}P′ for some P′ such that P′ ⊧ φ. Since P ∼ Q, we have Q⟶_{u}Q′ for some Q′ such that P′ ∼ Q′. By induction, Q′ ⊧ φ. So Q ⊧ ⟨u⟩φ. □

The converse of the proposition also holds for those processes which are called image-finite. We first introduce the notion of image-finite processes.

Definition 4.6.3 We say an agent P is image-finite if for every action α ∈ Act and u ∈ T ,

P_{α} = {P′ : P ⟶^{α}_{u}P′}

is finite and every P′ ∈ P_{α} is also image-finite.

Theorem 4.6.4 For any agents P and Q, if P or Q is image-finite and for any formula ψ, P ⊧ ψ if and only if Q ⊧ ψ, then P ∼ Q.

Proof: We write P =_{L} Q to represent that for every formula ψ of L, P ⊧ ψ if and only if Q ⊧ ψ. We only need to show that

S = {(P, Q) : P =_{L} Q & P or Q is image − finite}

is a strong bisimulation.

Suppose (P, Q) ∈ S. We first assume Q is image-finite.

(1) Suppose P ⟶^{α}_{u}P′. We further assume that Q⟶^{α}_{u}Q′ implies (P′, Q′) ∉ S. Let (Q_{1}, ⋯, Q_{n}) is an enumeration of {Q′ : Q⟶^{α}_{u}Q′}, where Q_{1}, ⋯, Q_{n} are image-finite. So P′ ≠_{L} Q_{i} for all i = 1, ⋯, n. Therefore, there are formulas ψ_{1}, ⋯, ψ_{n} such that P′ ⊧ ψ_{i} but Q_{i} |̸= ψ_{i}. Let ψ = ⟨u⟩⟨α, 0⟩(ψ_{1} ∧ ⋯∧ ψ_{n}). Then P ⊧ ψ but Q |̸= ψ, a contradiction. Hence there is a Q′ such that Q⟶^{α}_{u}Q′ and (P′, Q′) ∈ S.

(2) The case of P ⟶_{u}P′ is similar to (1).

Now assume P is image-finite. Suppose P ⟶^{α}_{u}P′, where P′ is image-finite. By the above, if Q⟶^{α}_{u}Q′′, then P ⟶^{α}_{u}P′′ and (P′′, Q′′) ∈ S for some P′′. Let {Q_{i} : i ∈

I} = {Q′ : Q⟶^{α}_{u}Q′} and {P_{1}, ⋯, P_{n}} = {P′′ : P ⟶^{α}_{u}P′′ &(P′′, Q_{i}) ∈ S &i ∈ I}.

Suppose (P′, Q_{i}) ∉ S for all i of I. Then (P′, P_{j}) ∉ S, where j = 1, ⋯, n. So there are formulas ψ_{1}, ⋯, ψ_{n} such that P′ ⊧ ψ_{i} but P_{i} |̸= ψ_{i} for all i = 1, ⋯, n. Let ψ = ⟨u⟩⟨α, 0⟩(ψ_{1} ∧ ⋯∧ ψ_{n}). Then P ⊧ ψ but Q |̸= ψ, a contradiction. Therefore there is a Q′ such that Q⟶^{α}_{u}Q′ and (P′, Q′) ∈ S. The case of P ⟶_{u}P′ is similar.

By symmetry, we have done. □

The above two theorems together are known as the modal characterization of bisimulation, which not only show that bisimulation is a natural equivalence, but also suggest that modal logic is an appropriate program logic for real-time systems.

The formulas of L can also be used to describe properties of real-time systems. As an example, we consider a vending machine which, after accepting coins, waits for a user to press a choice button for tea or coffee. If the user does not press the choice button within 5 minutes, the machine will refund the coins after another delay of Δ (Δ < 1 second) time and then return to its initial state waiting to serve other users. If the user presses the choice button at a right time (i.e. within 5 minutes), he can collect his tea or coffee after another Δ delay. After the user collects the drink, the machine return to its initial state. We can define the vending machine in Timed CCS as follows:

V M =^{def} coin(t)_{0}^{∞}. (choice(t)_{0}^{5}. collect(t)_{Δ}^{∞}. V M + refund(t)_{5+Δ}^{5+Δ}. V M)

Now we can express many interesting temporal properties of the vending machine as formulas of L as follows:

(1) the machine can receive coins at any time.

V M ⊧ ⟨coin, ∞⟩tt

(2) after inserting some coin, the user can make a choice within 5 minutes.

V M ⊧ [coin, ∞]⟨choice, 5⟩tt

(3) after the coins are inserted and a choice is made at a right time, the user can always get some drink and the coins will never be refunded.

V M ⊧ [coin, ∞][choice, 5](⟨collect, ∞⟩tt ∧ [refund, ∞]ff)

(4) after the coins are inserted and 5 + Δ minutes passes, the choice is timed out and the coins are refunded immediately.

V M ⊧ [coin, ∞][5 + Δ]([choice, ∞]ff ∧ ⟨refund, 0⟩tt)

Decidability

A variety of equivalences have been proposed in the field of process theory in order to capture the behavioural aspects of processes. Various criteria exist for comparing the merits and deficiencies of these equivalence. One of the most important criteria is decidability. For CCS, every finite process has only finite derivatives and therefore the decidability of the strong equivalence (for finite processes) is straightforward. However for real-time calculi, even simple finite processes may have infinite derivatives. In this chapter, we show that strong equivalence is still decidable over finite processes of real-time calculi. The decidability is independent of the choice of time domain, allowing time to be discrete or dense. In the rest of this chapter, we focus on finite processes, i.e. processes without recursion.

There are other works on decidability for real-time systems. In [HLW91], it is showed that strong bisimulations over regular processes without time variables is decidable. It also discusses model checking for a timed extension of Hennessy-Milner Logic. The work of [Cer92] generalises that of [HLW91] to also include parallel composition. It also discusses the decidability property for weak bisimulation. All these works are for real-time processes without time variables. In [AD90], it is showed that for timed Büchi automata the language emptiness problem is decidable but language inclusion problem is not. In [ACD90], a model checking algorithm for a real-time extension of branching time temporal logic is proposed. In [CM92], a tableau system for model checking of a real-time extension of Hennessy-Milner Logic with recursion is presented.

5.1 Characteristic Formulas

For any processes E and F, we construct a formula W C(E, F), the characteristic formula of E and F, of the first-order theory of some structure such that E ∼ F if and only if W C(E, F).

Definition 5.1.1 For any processes E and F, which contain at most free time variables t⃗ = (t_{1}, …, t_{n}), and a formula A, where fv(A) ⊆ {t_{1}, …, t_{n}}, we say A is a condition for E to be bisimilar to F, written as A ⊧ E ∼ F, if for any u⃗ ∈ T^{n}, A{u⃗/t⃗} implies E{u⃗/t⃗} ∼ F {u⃗/t⃗}.

Definition 5.1.2 A formula A is said to be a weakest condition for E to be bisimilar to F if A ⊧ E ∼ F and for any formula B, B ⊧ E ∼ F implies B → A holds.

Proposition 5.1.3 If A is a weakest condition for E to be bisimilar to F, then

B ⊧ P ∼ Q if and only if B → A

Proof: Straightforward. □

Corollary 5.1.4 If A and B are weakest conditions for E to be bisimilar to F, then A ↔ B holds.

We identify formulas which are logically equivalent. By the above corollary, we have that if weakest conditions for E to be bisimilar to F exist, then they are unique up to this equality.

Now we show that for all processes E and F, the weakest condition for E to be bisimilar to F exists. We first consider the weakest condition W C(E, F) for E to be bisimilar to F, where E and F are both in normal form.

Definition 5.1.5 For any normal forms E and F, where

E ≡ ∑_{i∈I} α_{i}(t_{i})_{e_{i}}^{e′_{i}}. E_{i} + (e)δ

and

F ≡ ∑_{j∈J} β_{j}(s_{j})_{f_{j}}^{f′_{j}}. F_{j} + (f)δ

let

W C(E, F) =^{def} (e = f)∧

⋀_{i∈I}(∀t(e_{i} ≤ t ≤ e′_{i} → ⋁_{j∈J^{α_{i}=β_{j}}}(f_{j} ≤ t ≤ f′_{j} ∧ W C(E_{i}{t/t_{i}}, F_{j}{t/s_{j}}))))∧

⋀_{j∈J}(∀s(f_{j} ≤ s ≤ f′_{j} → ⋁_{i∈I^{α_{i}=β_{j}}}(e_{i} ≤ s ≤ e′_{i} ∧ W C(E_{i}{s/t_{i}}, F_{j}{s/s_{j}}))))

We will show that W C(E, F) is the weakest condition for E to be bisimilar to F, where E and F are both in normal form. We first show that W C(E, F) is a condition for E to be bisimilar to F.

Proposition 5.1.6 For any normal forms E and F, W C(E, F) ⊧ E ∼ F.

Proof: For normal forms E ≡ ∑_{i∈I} α_{i}(t_{i})_{e_{i}}^{e′_{i}}. E_{i}+(e)δ and F ≡ ∑_{j∈J} β_{j}(s_{j})_{f_{j}}^{f′_{j}}. F_{j} + (f)δ, suppose E and F contain at most free time variables r⃗ = (r_{1}, …, r_{n}). We proceed by induction on the maximum depth of E and F, where the depth d(E) of E is inductively defined as follows:

\begin{matrix}d((e)δ) = 0 & d(α(t)_{e}^{e′}. E) = 1 + d(E) \\ d(E + F) = max(d(E), d(F)) \end{matrix}

For any u⃗ = (u_{1}, …, u_{n}) ∈ T^{n}, we suppose W C(E, F){u⃗/r⃗} holds.

Firstly, E{u⃗/r⃗}⟶^{α}_{v}P′, then there is i ∈ I such that α = α_{i}, e_{i}{u⃗/r⃗} ≤ v ≤ e′_{i}{u⃗/r⃗} and P′ ≡ E_{i}{u⃗/r⃗}{v/t_{i}}. By definition of W C(E, F), there is j ∈ J, such that β_{j} = α_{i}, f_{j}{u⃗/r⃗} ≤ v ≤ f′_{j}{u⃗/r⃗} and W C(E_{i}{u⃗/r⃗}{v/t_{i}}, F_{j}{u⃗/r⃗}{v/s_{j}}) holds. By induction, we have E_{i}{u⃗/r⃗}{v/t_{i}} ∼ F_{j}{u⃗/r⃗}{v/s_{j}}) hold. Clearly

F {u⃗/r⃗}⟶^{β_{j}}_{v}F_{j}{u⃗/r⃗}{v/s_{j}}.

Similarly, F {u⃗/r⃗}⟶^{α}_{v}Q′ implies E{u⃗/t⃗}⟶^{α}_{v}P′ with P′ ∼ Q′ for some P′.

Finally, e{u⃗/r⃗} = f{u⃗/r⃗}. Therefore E{u⃗/r⃗} ∼ F {u⃗/r⃗}. □

Now we show that W C(E, F), where E and F are both in normal form, is the weakest condition for E to be bisimilar to F. To do so we first prove the following lemma.

Lemma 5.1.7 For any normal forms E and F, E ∼ F implies W C(E, F).

Proof: We only need to consider the case where both E and F are agents. Let E ≡ ∑_{i∈I} α_{i}(t_{i})_{v_{i}}^{v′_{i}}. E_{i} + (v)δ and F ≡ ∑_{j∈J} β_{j}(s_{j})_{w_{j}}^{w′_{j}}. F_{j} + (w)δ be normal forms. Suppose E ∼ F. We proceed by induction on the maximum depth m of E and F.

Case m = 0. Then we have E ≡ (v)δ and F ≡ (w)δ. Clearly E ∼ F implies v = w.

Case m = m′ + 1.

(1) For any i ∈ I, if v_{i} ≤ u ≤ v′_{i}, then we have E⟶^{α_{i}}_{u}E_{i}{u/t_{i}}. So there

is a j ∈ J such that F ⟶^{β_{j}}_{u}F_{j}{u/s_{j}} and F_{j}{u/s_{j}} ∼ E_{i}{u/t_{i}}, where

α_{i} = β_{j} and w_{j} ≤ u ≤ w′_{j}. By induction, W C(F_{j}{u/s_{j}}, E_{i}{u/t_{i}}) holds.

(2) Similarly, for any j ∈ J, w_{j} ≤ u ≤ w′_{j} implies that there is a i ∈ I such that v_{i} ≤ u ≤ v′_{i} and W C(F_{j}{u/s_{j}}, E_{i}{u/t_{i}}) hold.

(3) v = w.

Therefore W C(E, F) holds □

Proposition 5.1.8 For normal forms E, F and formula A, A ⊧ E ∼ F implies A → W C(E, F) holds.

Proof: For any normal forms E ≡ ∑_{i∈I} α_{i}(t_{i})_{e_{i}}^{e′_{i}}. E_{i}+(e)δ and F ≡ ∑_{j∈J} β_{j}(s_{j})_{f_{j}}^{f′_{j}}. F_{j}+ (f)δ, suppose E and F contain at most time variables r⃗ = (r_{1}, …, r_{n}) and A ⊧ E ∼ F. For any u⃗ = (u_{1}, …, u_{n}) ∈ T^{n}, if A{u⃗/r⃗} holds, then E{u⃗/t⃗} ∼ F {u⃗/r⃗}. By Lemma 5.1.7, W C(E{u⃗/r⃗}, F {u⃗/r⃗}) holds. Hence A → W C(E, F) holds. □

Corollary 5.1.9 For normal forms E, E′ and F, E ∼ E′ implies that W C(E, F) is logically equivalent to W C(E′, F).

Now we consider the weakest condition for E to be bisimilar to F, for any processes E and F. We first show that for any process E, there is a normal form F such that E ∼ F.

Lemma 5.1.10 For any process E, there is a normal form F such that E ∼ F.

Proof: Since for every process E, there is a process E′, where E′ does not contain the restriction operator (except δ), relabelling operator and parallel operator, such that E ∼ E′, we only need to show that for every such E′ there is a normal form F such that E′ ∼ F. We proceed by induction on the structure of E′.

– E′ ≡ (e)δ, trivial.

– E′ ≡ α(t)_{e}^{e′}. E′′. By induction, there is a normal form F′′ such that E′′ ∼ F′′. So we have α(t)_{e}^{e′}. E′′ ∼ α(t)_{e}^{e′}. F′′ + (e′)δ.

– E′ ≡ E_{1}+E_{2}. By induction, there are normal forms F_{1} ≡ ∑_{i∈I} α_{i}(t_{i})_{e_{i}}^{e′_{i}}. F_{1i}+(e)δ and F_{2} ≡ ∑_{j∈J} β_{j}(t_{j})_{f_{j}}^{f′_{j}}. F_{2j} + (f)δ such that E_{1} ∼ F_{1} and E_{2} ∼ F_{2}. Clearly F ≡ ∑_{i∈I} α_{i}(t_{i})_{e_{i}}^{e′_{i}}. F_{1i} + ∑_{j∈J} β_{j}(t_{j})_{f_{j}}^{f′_{j}}. F_{2j} + (max(e, f))δ is in normal form and E′ ∼ F. □

Definition 5.1.11 For any processes E and F, let W C(E, F) be W C(E′, F′), where normal forms E′ and F′ satisfy E ∼ E′ and F ∼ F′.

Clearly W C(E, F) is well defined. We will show next that W C(E, F) is the weakest condition for E to be bisimilar to F.

Proposition 5.1.12 For any processes E and F, W C(E, F) is the weakest condition for E to be bisimilar to F.

Proof: We first show that W C(E, F) is a condition for E to be bisimilar to F, i.e. W C(E, F) ⊧ E ∼ F holds. Suppose E and F contain at most free time variables t⃗ = (t_{1}, ⋯, t_{n}). Let E′ and F′ be normal forms such that E ∼ E′ and F ∼ F′. For any u⃗ ∈ T^{n}, suppose W C(E, F){u⃗/t⃗} holds. Then E′{u⃗/t⃗} ∼ F′{u⃗/t⃗}. So E{u⃗/t⃗} ∼ F {u⃗/t⃗} holds.

Now we suppose A ⊧ E ∼ F holds. We further assume A{u⃗/t⃗} holds, where u⃗ ∈ T^{n}. Then E{u⃗/t⃗} ∼ F {u⃗/t⃗}. So E′{u⃗/t⃗} ∼ F′{u⃗/t⃗} and therefore W C(E, F){u⃗/t⃗}. □

5.2 Decidability over Discrete Time Domains

In this section, we suppose time is discrete. Let T be , the set of natural numbers.

In the structure ( , +), we can define the following relations:

(1) Zero ({m : m = 0}): ∀x(x + m = x)

(2) Ordering ({(m, n) : m ≤ n}): ∃x(m + x = n)

(3) Successor ({(m, n) : n = S(m)}):

∃x∀y(x ≠ 0) ∧ (y = 0 ∨ x ≤ y) ∧ m + x = n

(4) Subtraction ({(l, m, n) : n = l ˙−m}): (l < m ∧ n = 0) ∨ (l ≥ m ∧ l = m + n)

(5) Max ({(l, m, n) : n = max(l, m)}): (l ≥ m ∧ n = l) ∨ (l < m ∧ n = m)

(6) Min ({(l, m, n) : n = min(l, m)}): (l ≥ m ∧ n = m) ∨ (l < m ∧ n = l)

For any time expression e over time domain (T ∪ {∞}, ≤), we have e < ∞. We can read the terms of the form e ≤ ∞ as 0 = 0 throughout W C(E, F). As a result, W C(E, F) is a sentence of the first-order theory over structure ( , +).

Theorem 5.2.1 ∼ is decidable for agents.

Proof: The result follows from the decidability of the first-order theory of the natural numbers with + [End72]. □

Lemma 5.2.2 For any processes E and F which contain at most free time variables t⃗ = (t_{1}, …, t_{n}), we have

E ∼ F if and only if ∀t_{1} … ∀t_{n}W C(E, F)

Proof: The result follows from the definition of strong equivalence over processes. □

Lemma 5.2.3 For any processes E and F, where E and F contain at most free time variables t_{1}, …, t_{n}, the formula ∀t_{1} … ∀t_{n}W C(E, F) is a sentence of the first-order theory over structure ( , +).

Proof: Straightforward. □

Theorem 5.2.4 ∼ is decidable.

Proof: Analogous to Theorem 5.2.1. □

Since the first-order theory of the natural numbers with + and ×, i.e. Th( , +, ×), is undecidable, this justifies our decisions in the choice of time expressions.

5.3 Decidability over Dense Time Domains

In this section, we assume time to be dense. Let T be ^{≥0}, the set of non-negative real numbers.

As for the structure ( , +), we can also define relations: Zero, Ordering, Subtraction, Max and Min in the structure ( , +, ×).

Lemma 5.3.1 For any processes E and F, where E and F contain at most free time variables t_{1}, …, t_{n}, the formula ∀t_{1} … ∀t_{n}W C(E, F) is a sentence of the first-order theory over structure ( , +, ×).

Proof: Straightforward. □

Theorem 5.3.2 ∼ is decidable.

Proof: The result follows from the decidability of the first-order theory of the reals with + and × [Col75].

A Proof System

In the last chapter we have shown that for any finite processes E and F, we have a characteristic formula W C(E, F) such that E ∼ F if and only if W C(E, F) holds. We used the notation A ⊧ E ∼ F to indicate that a formula A is a condition for process E to be bisimilar to process F. In this section, we study proof systems for strong equivalence.

There is a simple proof system for strong equivalence pointed out by Kim Larsen which consists of a single rule

\frac{W C(E, F)}{E = F}

The proof system is independent of the choice of time domain, allowing time to be discrete or dense. It is sound and complete for finite processes over discrete time as well as dense time domains.

In this chapter we describe a relativised compositional proof system in which we derive statements of the form A ⊢ E = F. The proof system is sound. It is complete for finite processes over dense time domains, but only complete for a restricted language over discrete time domains. We will give some examples to show how the proof system works for finite processes as well as recursively defined processes.

6.1 The Proof System

In the rest of this chapter, we will mainly focus on finite processes (except Section 6.4 in which we will discuss how the proof system works for recursively defined processes). By Lemma 5.1.10, for every finite process E, we have a normal form F such that E ∼ F. However, every finite normal form can be defined by the following BNF expressions:

E ::= δ |nil |(e)E |α(t)_{e}^{e′}. E |E + F

where e is a time expression and e′ is a time expression or ∞.

Henceforth we will focus on the sublanguage defined by the above syntax except Section 6.4. We first present the proof system. Table 6–1 contains all axioms and Table 6–2 contains all proof rules. The proof rules are in the form

\frac{S_{1} … S_{n}}{S}

where S_{1}, …, S_{n}, S are statements. The rule can be read as: if all premises S_{1}, …, S_{n} can be derived, then the conclusion S can be deduced.

We say A ⊢ X = Y is derivable if it can be derived from the axioms in Table 6– 1 by using the proof rules in Table 6–2. For convenience, we write A ⊢ X = Y to assert that A ⊢ X = Y is derivable.

Lemma 6.1.1 The following are derivable:

(1) e ≤ f ∧ f ≤ f′ ∧ f′ ≤ e′ ⊢ α(t)_{f}^{f′}. E + α(t)_{e}^{e′}. E = α(t)_{e}^{e′}. E

(2) e ≤ f ∧ f ≤ e′ ∧ e′ ≤ f′ ⊢ α(t)_{f}^{f′}. E + α(t)_{e}^{e′}. E = α(t)_{e}^{f′}. E

Proof: We only consider (1), as (2) is similar. For (1), we have

e ≤ f ≤ e′ ⊢ α(t)_{e}^{e′}. E = α(t)_{e}^{f}. E + α(t)_{f}^{e′}. E

false ⊢ X = Y  true ⊢ X = X
true ⊢ X = X + δ  true ⊢ X = X + X
true ⊢ X + Y = Y + X  true ⊢ X + (Y + Z) = (X + Y) + Z
true ⊢ X = (0)X  true ⊢ (e)(e′)δ = (e + e′)δ
true ⊢ (e)(X + Y) = (e)X + (e)Y true ⊢ α(t)_{e}^{e′}. X = α(t)_{e}^{e′}. X + (e′)δ

e′ < e ⊢ α(t)_{e}^{e′}. X = (e′)δ

e ≤ s ≤ e′ ⊢ α(t)_{e}^{e′}. X = α(t)_{e}^{s}. X + α(t)_{s}^{e′}. X

true ⊢ α(t){e′ \atop e}. X = α(s){e′ \atop e}. X\{s/t\} (s is free for t in X)

true ⊢ (e)(α(t)_{f}^{f′}. X) = α(t)_{f+e}^{f′+e}. X{t − e/t} (t ∉ fv(e))

Table 6–1: Axioms

1  \frac{A ⊢ X = Y  A ⊢ Y = Z}{A ⊢ X = Z}

2  \frac{A ⊢ X = Y  B ⊢ X = Y}{A ∨ B ⊢ X = Y}

3  \frac{B ⊢ X = Y}{A ⊢ X = Y}  (A → B)

4 \frac{A ⊢ X = Y}{A ∧ e = f ⊢ (e)X = (f)Y}

5  \frac{A ∧ e ≤ t ≤ e′ ⊢ X = Y}{A ∧ e = f ∧ e′ = f′ ⊢ α(t)_{e}^{e′}. X = α(t)_{f}^{f′}. Y}  (t ∉ fv(A))

6  \frac{A ⊢ X = Y  A ⊢ X′ = Y′}{A ⊢ X + X′ = Y + Y′}

7  \frac{A ⊢ X = Y  B ⊢ X = Z}{A ∨ B ⊢ X + Y + Z = Y + Z}

Table 6–2: Proof Rules Chapter 6. A Proof System 95

f ≤ f′ ≤ e′ ⊢ α(t)_{f}^{e′}. E = α(t)_{f}^{f′}. E + α(t)_{f′}^{e′}. E

Clearly

e ≤ f ∧ f ≤ f′ ∧ f′ ≤ e′ → e ≤ f ≤ e′

and

e ≤ f ∧ f ≤ f′ ∧ f′ ≤ e′ → f ≤ f′ ≤ e′

So

e ≤ f ∧ f ≤ f′ ∧ f′ ≤ e′ ⊢ α(t)_{e}^{e′}. E = α(t)_{e}^{f}. E + α(t)_{f}^{e′}. E

and

e ≤ f ∧ f ≤ f′ ∧ f′ ≤ e′ ⊢ α(t)_{f}^{e′}. E = α(t)_{f}^{f′}. E + α(t)_{f′}^{e′}. E

Thus

e ≤ f ∧ f ≤ f′ ∧ f′ ≤ e′ ⊢ α(t)_{f}^{e′}. E = α(t)_{f}^{e′}. E + α(t)_{f}^{f′}. E

and

e ≤ f ∧ f ≤ f′ ∧ f′ ≤ e′ ⊢ α(t)_{e}^{e′}. E = α(t)_{e}^{e′}. E + α(t)_{f}^{f′}. E □

Lemma 6.1.2

(1) If A ⊢ X = Y and t ∉ fv(A), then A ∧ (e ≤ t ≤ e′) ⊢ α(t)_{e}^{e′}. X = α(t)_{e}^{e′}. Y.

(2) If A ⊢ X = Y and t ∉ fv(A), then A ∧ e = f ∧ e′ = f′ ⊢ α(t)_{e}^{e′}. X = α(t)_{f}^{f′}. Y. Proof: We only consider (2), as (1) is similar.

Suppose A ⊢ X = Y and t ∉ fv(A). Since A ∧ e ≤ t ≤ e′ → A, we have A ∧ e ≤ t ≤ e′ ⊢ X = Y. Thus A ∧ e = f ∧ e′ = f′ ⊢ α(t)_{e}^{e′}. X = α(t)_{f}^{f′}. Y. □

Remark Rules (1) and (2) of Lemma 6.1.2 are equipotent with the proof rule 5. In fact they were the version which I first proposed. □

For convenience, we will write ⊢ E = F in place of true ⊢ E = F.

Now we consider a simple example and show how the proof system works. In Section 6.4, we will consider a more interesting example and show how the proof system works for recursively defined processes.

Example Let E ≡ b(s)_{0}^{t−(2 ˙−t)}. δ, F ≡ b(s)_{0}^{2t−2}. δ and G ≡ b(s)_{0}^{t}. δ. We show that

⊢ a(t)_{1}^{10}. (E + F + G) = a(t)_{1}^{10}. (F + G)

is derivable.

\frac{⊢ δ = δ}{\frac{t − (2 ˙−t) = 2t − 2 ⊢ b(s)_{0}^{t−(2 ˙−t)}. δ = b(s)_{0}^{2t−2}. δ}{t ≤ 2 ⊢ b(s)_{0}^{t−(2 ˙−t)}. δ = b(s)_{0}^{2t−2}. δ} t ≤ 2 → (t − (2 ˙−t) = 2t − 2)}

and

\frac{⊢ δ = δ}{\frac{t − (2 ˙−t) = t ⊢ b(s)_{0}^{t−(2 ˙−t)}. δ = b(s)_{0}^{t}. δ}{t > 2 ⊢ b(s)_{0}^{t−(2 ˙−t)}. δ = b(s)_{0}^{t}. δ} t > 2 → (t − (2 ˙−t) = t)}

By rule 7

t ≤ 2 ∨ t > 2 ⊢ E + F + G = F + G

and

\frac{\frac{t ≤ 2 ∨ t > 2 ⊢ E + F + G = F + G}{1 ≤ t ≤ 10 ⊢ E + F + G = F + G} 1 ≤ t ≤ 10 → (t ≤ 2 ∨ t > 2)}{⊢ a(t)_{1}^{10}. (E + F + G) = a(t)_{1}^{10}. (F + G)}

6.2 Soundness

The soundness of the proof system is shown by the following proposition.

Proposition 6.2.1 (Soundness) If A ⊢ E = F, then A ⊧ E ∼ F.

Proof: We only need to show that every instance of the axioms of Table 6–1 is valid, i.e. if A ⊢ E = F is an instance of an axiom, then A ⊧ E ∼ F, and every proof rule of Table 6–2 preserves the validity. The validity of every instance of the axioms follows from the properties of strong bisimulation (see Chapter 4 for details).

The proofs of rules (1), (2), (3) and (4) are straightforward.

For (5), we suppose A ∧ e ≤ t ≤ e′ ⊧ X ∼ Y where the formula A and the processes α(t)_{e}^{e′}. X, α(t)_{f}^{f′}. Y contain at most free time variables s⃗ = (s_{1}, ⋯, s_{n}). For any v⃗ ∈ T^{n}, we also suppose A{v⃗/s⃗} holds, e{v⃗/s⃗} = f{v⃗/s⃗} and e′{v⃗/s⃗} =

f′{v⃗/s⃗}. If (α(t)_{e}^{e′}. X){v⃗/s⃗}⟶^{β}_{u}P′, then β = α, and P′ ≡ X{v⃗/s⃗}{u/t} where

e{v⃗/s⃗} ≤ u ≤ e′{v⃗/s⃗}. Clearly (α(t)_{f}^{f′}. Y){v⃗/s⃗}⟶^{α}_{u}Y {v⃗/s⃗}{u/t} and X{v⃗/s⃗}{u/t} ∼

Y {v⃗/s⃗}{u/t} (note that t ∉ fv(A)). By symmetry, we finish the proof of rule (5).

For (6), we suppose A ⊧ X ∼ Y and A ⊧ X′ ∼ Y′. Let the formula A, the processes X, X′, Y and Y′ contain at most free time variables s⃗ = (s_{1}, ⋯, s_{n}). For any v⃗ ∈ T^{n}, we also suppose A{v⃗/s⃗} holds. So we have X{v⃗/s⃗} ∼ Y {v⃗/s⃗} and X′{v⃗/s⃗} ∼ Y′{v⃗/s⃗}. Therefore (X + X′){v⃗/s⃗} ∼ (Y + Y′){v⃗/s⃗}.

The proof of rule (7) is similar to that of rule (6). □

Note that the side condition of rule 5 is important, as otherwise the rule is invalid. As an example, let the formula A be 1 ≤ t ≤ 5, the processes X and Y be b(s)_{0}^{10−t}. nil and b(s)_{0}^{t}. nil, respectively. Clearly we have A ∧ 5 ≤ t ≤ 10 ⊧ X ∼ Y, but A |̸= a(t)_{5}^{10}. X ∼ a(t)_{5}^{10}. Y.

6.3 Completeness

The completeness result of the proof system depends heavily on the existence of normal forms. Lemma 6.3.1 For any process E, there is a normal form E′ such that ⊢ E = E′. Proof: We proceed by induction on the structure of E. Case 1 E ≡ δ. Clearly ⊢ δ = (0)δ. Case 2 E ≡ nil. Clearly ⊢ (∞)δ = (∞)δ. Case 3 E ≡ (f)F. By induction, there is a normal form ∑_{i∈I} α_{i}(t_{i})_{e_{i}}^{e′_{i}}. E_{i} + (e)δ

such that

⊢ F = ∑_{i∈I} α_{i}(t_{i})_{e_{i}}^{e′_{i}}. E_{i} + (e)δ

So

⊢ (f)F = (f)(∑_{i∈I} α_{i}(t_{i})_{e_{i}}^{e′_{i}}. F_{i} + (e)δ)

Therefore

⊢ (f)F = ∑_{i∈I} α_{i}(t_{i})_{e_{i}+f}^{e′_{i}+f}. E_{i}{t_{i} − f/t_{i}} + (e + f)δ

and ∑_{i∈I} α_{i}(t_{i})_{e_{i}+f}^{e′_{i}+f}. E_{i}{t_{i} − f/t_{i}} + (e + f)δ is in normal form. Case 4 E ≡ α(t)_{e}^{e′}. F. By induction, there is a normal form F′ such that ⊢ F =

F′. So ⊢ α(t)_{e}^{e′}. F = α(t)_{e}^{e′}. F′ and therefore ⊢ α(t)_{e}^{e′}. F = a(t)_{e}^{e′}. F′ + (e′)δ

where a(t)_{e}^{e′}. F′ + (e′)δ is in normal form.

Case 5 E ≡ E_{1} + E_{2}. By induction, there is a normal form ∑_{i∈I} α_{i}(t_{i})_{e_{i}}^{e′_{i}}. E′_{i} + (e)δ

such that

⊢ E_{1} = ∑_{i∈I} α_{i}(t_{i})_{e_{i}}^{e′_{i}}. E′_{i} + (e)δ

and a normal form ∑_{j∈J} β_{j}(s_{j})_{f_{j}}^{f′_{j}}. E′′_{j} + (f)δ such that

⊢ E_{2} = ∑_{j∈J} β_{j}(s_{j})_{f_{j}}^{f′_{j}}. E′′_{j} + (f)δ

So

⊢ E_{1} + E_{2} = ∑_{i∈I} α_{i}(t_{i})_{e_{i}}^{e′_{i}}. E′_{i} + ∑_{j∈J} β_{j}(s_{j})_{f_{j}}^{f′_{j}}. E′′_{j} + (max(e, f))δ

where ∑_{i∈I} α_{i}(t_{i})_{e_{i}}^{e′_{i}}. E′_{i} + ∑_{j∈J} β_{j}(s_{j})_{f_{j}}^{f′_{j}}. E′′_{j} + (max(e, f))δ is in a normal form.

□

6.3.1 Completeness in Dense Time Domains

In this section, we assume time to be dense. For example, the time domain is ( ^{≥0} ∪ {∞}, ≤) or ( ^{≥0} ∪ {∞}, ≤). By Lemma 6.3.1, we can further assume that every process is in normal form.

We first show that for any processes E and F, the weakest condition for E to be bisimilar to F can be written in disjunctive normal form.

Lemma 6.3.2 For any processes E and F which contain at most free time variables (t_{1}, …, t_{n}), W C(E, F) can be written in disjunctive normal form

⋁_{i∈I} e_{1i} ≤ t_{1} ≤ f_{1i} ∧ ⋯ ∧ e_{ni}(t_{1}, …, t_{n−1}) ≤ t_{n} ≤ f_{ni}(t_{1}, …, t_{n−1})

for some finite I, where e_{ki}(t_{1}, ⋯, t_{k−1}) and f_{ki}(t_{1}, ⋯, t_{k−1}) (k = 1, ⋯, n) contain at most variables t_{1}, ⋯, t_{k−1}.

Proof: We proceed by induction on the maximal depth of E and F.

For the base case, we have W C(E, F) ≡ (e = f). If e = e′ + ut, where u is a constant (i.e. u ∈ T), t ∉ fv(e′) and t ∉ fv(f), then e = f can be replaced by (f ˙−e′)u^{−1} ≤ t ≤ (f − e′)u^{−1} which clearly can be written in the above form. If e = e′ ˙−u×t, where u ∈ T, t ∉ fv(e′) and t ∉ fv(f), then e = f can be replaced by Chapter 6. A Proof System 100 ((u^{−1}×e′ ≤ t ≤ ∞)∧0 = f)∨((0 ≤ t ≤ u^{−1}×e′)∧u^{−1}×(e′ ˙−f) ≤ t ≤ u^{−1}×(e′−f) which can also be written in the above form. All other cases are similar.

For the inductive case, we have W C(E, F) ≡ (e = f) ∧

⋀_{i∈I}(∀t(e_{i} ≤ t ≤ e′_{i} → ⋁_{α_{i}=β_{j}^{j∈J}}(f_{j} ≤ t ≤ f′_{j} ∧ W C(E_{i}{t/t_{i}}, F_{j}{t/s_{j}}))))

⋀_{j∈J}(∀s(f_{j} ≤ s ≤ f′_{j} → ⋁_{α_{i}=β_{j}^{i∈I}}(e_{i} ≤ s ≤ e′_{i} ∧ W C(E_{i}{s/t_{i}}, F_{j}{s/s_{j}}))))

For any i ∈ I and j ∈ J, by induction

W C(E_{i}{t/t_{i}}, F_{j}{t/s_{j}}) = ⋁_{l∈L}(g_{l} ≤ t ≤ g′_{l}) ∧ D_{ij}^{l}

where for every l ∈ L, t ∉ fv(D_{ij}^{l}) and L is finite, and

W C(E_{i}{s/t_{i}}, F_{j}{s/s_{j}}) = ⋁_{k∈K}(h_{k} ≤ s ≤ h′_{k}) ∧ C_{ij}^{k}

where for every k ∈ K, s ∉ fv(C_{ij}^{k}) and K is finite. So W C(E, F) = (e = f)∧

⋀_{i∈I} ∀t(e_{i} ≤ t ≤ e′_{i} → ⋁_{α_{i}=β_{j}^{l∈L}^{j∈J}}(max(f_{i}, g_{l}) ≤ t ≤ min(f′_{j}, g′_{l}) ∧ D_{ij}^{l}))

⋀_{j∈J} ∀s(max(0, f_{j}) ≤ s ≤ f′_{j} → ⋁_{α_{i}=β_{j}^{k∈K}^{i∈I}}(max(e_{i}, h_{k}) ≤ s ≤ min(e′_{i}, h′_{k}) ∧ C_{ij}^{k}))

For any i ∈ I, we may replace

∀t(e_{i} ≤ t ≤ e′_{i} → ⋁_{α_{i}=β_{j}^{l∈L}^{j∈J}}(max(f_{i}, g_{l}) ≤ t ≤ min(f′_{j}, g′_{l}) ∧ D_{ij}^{l}))

by

∀t( ⋁_{⋮ ; (u_{n}, v_{n}) ∈ Inv^{(u_{1},v_{1})∈Inv}}(e_{i} ≥ u_{1} ∧ u_{1} ≤ v_{1} ∧ u_{2} ≤ v_{1} ≤ v_{2} ∧ ⋯∧

u_{n} ≤ v_{n−1} ≤ v_{n} ∧ v_{n} ≥ e′_{i} ∧ ⋀_{j∈J^{l∈L′}} D_{ij}^{l}))

where

Inv = {(max(f_{j}, g_{l}), min(f′_{j}, g′_{l})) : j ∈ J, l ∈ L}
L′ = {l : max(f_{j}, g_{l}) ∈ {u_{1}, …, u_{n}}}

in W C(E, F).

Since t ∉ fv({e_{i}, e′_{i}, f_{j}, f′_{j}, g_{l}, g′_{l}, D_{ij}^{l′} : j ∈ J, l ∈ L, l′ ∈ L′}), the result can further be replaced by

⋁_{⋮^{(u_{1},v_{1})∈Inv} ; (u_{n}, v_{n}) ∈ Inv}(e_{i} ≥ u_{1} ∧ u_{1} ≤ v_{1} ∧ u_{2} ≤ v_{1} ≤ v_{2} ∧ ⋯∧

u_{n} ≤ v_{n−1} ≤ v_{n} ∧ v_{n} ≥ e′_{i} ⋀_{j∈J^{l∈L′}} D_{ij}^{l})

For the other parts, we can do the same replacement. It is easy to show that the final result can be written in the required disjunctive normal form. □

Remark For discrete time domains, the lemma in general does not hold. For example, the formula 3t = 5s cannot be written in the required form. In the next section, we will show how to restrict the occurrences of time variables in time expressions such that we can still retain the lemma for discrete time domains. □

Proposition 6.3.3 For any processes E and F, W C(E, F) ⊢ E = F.

Proof: We proceed by induction on the maximal depth of E and F.

For the base case, we have E ≡ (e)δ and F ≡ (f)δ. Then W C(E, F) ≡ (e = f) and e = f ⊢ E = F.

For the inductive case, we have Chapter 6. A Proof System 102

E ≡ ∑_{i∈I} α_{i}(t_{i})_{e_{i}}^{e′_{i}}. E_{i} + (e)δ and F ≡ ∑_{j∈J} β_{j}(s_{j})_{f_{j}}^{f′_{j}}. F_{j} + (f)δ

Suppose I ≠ ∅. If J = ∅, then F ≡ (f)δ and

W C(E, F) ↔ (e = f) ∧ ⋀_{i∈I}(e_{i} > e′_{i})

Clearly

(e = f) ∧ ⋀_{i∈I}(e_{i} > e′_{i}) ⊢ E = F

Hence W C(E, F) ⊢ E = F.

Now suppose J ≠ ∅, for any i ∈ I, j ∈ J, by induction

W C(E_{i}{t/t_{i}}, F_{j}{t/s_{j}}) ⊢ E_{i}{t/t_{i}} = F_{j}{t/s_{j}}

By the lemma, W C(E_{i}{t/t_{i}}, F_{j}{t/s_{j}}) can be written as

⋁_{l∈L}(g_{l} ≤ t ≤ g′_{l} ∧ D_{ij}^{l})

where for any l ∈ L, t ∉ fv(D_{ij}^{l}). So, for any l ∈ L

g_{l} ≤ t ≤ g′_{l} ∧ D_{ij}^{l} ⊢ E_{i}{t/t_{i}} = F_{i}{t/s_{j}}

Thus

(max(e_{i}, f_{j}, g_{l}) ≤ t ≤ min(e′_{i}, f′_{j}, g′_{l})) ∧ D_{ij}^{l} ⊢ E_{i}{t/t_{i}} = F_{i}{t/s_{j}}

and

D_{ij}^{l} ⊢ α_{i}(t_{i})_{max(e_{i},f_{j},g_{l})}^{min(e′_{i},f′_{j},g′_{l})}. E_{i} = α_{i}(s_{j})_{max(e_{i},f_{j},g_{l})}^{min(e′_{i},f′_{j},g′_{l})}. F_{j}

Let Inv = {(max(f_{j}, g_{l}), min(f′_{l}, g′_{j})) : j ∈ J&l ∈ L}. For any (u_{1}, v_{1}), …, (u_{n}, v_{n}) ∈ Inv, let

C = e_{i} ≥ u_{1} ∧ u_{1} ≤ u_{2} ≤ v_{1} ∧ ⋯ ∧ u_{n−1} ≤ u_{n} ∧ u_{n} ≤ v_{n−1} ≤ v_{n} ∧ v_{n} ≥ e′_{i} Then

C ⊢ α_{i}(t_{i})_{e_{i}}^{e′_{i}}. E_{i} = ∑_{k=1}^{n} α_{i}(t_{i})_{max(e_{i},u_{k})}^{min(e′_{i},v_{k})}. E_{i}

Chapter 6. A Proof System 103 and

( ⋀_{l∈L′} D_{ij}^{l}) ∧ C ⊢ α_{i}(t_{i})_{e_{i}}^{e′_{i}}. E_{i} = ∑_{α_{i}=β_{π(k)}^{k=1}}^{n} β_{π(k)}(s_{π(k)})_{max(e_{i},u_{k})}^{min(e′_{i},v_{k})}. F_{π(k)}

where L′ = {l : max(f_{j}, g_{l}) ∈ {u_{1}, …, u_{n}}} and π(k) = j where u_{k} = max(f_{j}, g_{l}). So

C ∧ ⋀_{l∈L′} D_{ij}^{l} ⊢ α_{i}(t_{i})_{e_{i}}^{e′_{i}}. E_{i} + F = F

and

⋁_{⋮^{(u_{1},v_{1})∈Inv} ; (u_{n}, v_{n}) ∈ Inv}( ⋀_{l∈L′} D_{ij}^{l} ∧ C) ⊢ α_{i}(t_{i})_{e_{i}}^{e′_{i}}. E_{i} + F = F

where

C ≡ e_{i} ≥ u_{1} ∧ u_{1} ≤ u_{2} ≤ v_{1} ∧ ⋯ ∧ u_{n−1} ≤ u_{n} ∧ u_{n} ≤ v_{n−1} ≤ v_{n} ∧ v_{n} ≥ e′_{i}

Hence

⋀_{i∈I}( ⋁_{⋮^{(u_{1},v_{1})∈Inv} ; (u_{n}, v_{n}) ∈ Inv}( ⋀_{l∈L′} D_{ij}^{l} ∧ C)) ∧ (e = f) ⊢ E + F = F

and

W C(E, F) ⊢ E + F = F

Similarly

W C(E, F) ⊢ E + F = E

So

W C(E, F) ⊢ E = F □

Corollary 6.3.4 A ⊧ E ∼ F implies A ⊢ E = F. Corollary 6.3.5 (Completeness) For any processes E and F,

E ∼ F implies ⊢ E = F

6.3.2 Completeness in Discrete Time Domains

In this section, we assume time to be discrete. For example, the time domain is ( ∪ {∞}, ≤), where is the set of natural numbers.

As shown in the last section, Lemma 6.3.2 in general does not hold for discrete time domains. As a result, the proof system is not complete for processes over discrete time domain ( ∪ {∞}, ≤). For example, consider processes E ≡ a(t)_{6}^{6}. b(s)_{10}^{10}. (3s)δ and F ≡ a(t)_{6}^{6}. b(s)_{10}^{10}. (5t)δ. Clearly we have ⊧ E ∼ F, but ⊢ E = F is not derivable using our proposed technique. However, if we restrict the occurrences of time variables in time expressions, we can still retain the lemma.

We first formalise a notion of time expressions of a process.

Notation Let e be a time expression and S be a set of time expressions. We write e + S in place of the set {e + f : f ∈ S} of time expressions. □

Definition 6.3.6 For any process E, the set of time expressions Exp_{1}(E) of E is inductively defined as follows:

Exp_{1}(δ) = {0}  Exp_{1}(a(t)_{e}^{e′}. E) = {e, e′}
Exp_{1}(nil) = {∞}  Exp_{1}(E + F) = Exp_{1}(E) ∪ Exp_{1}(F)
Exp_{1}((e)E) = e + Exp_{1}(E)

Definition 6.3.7 For any process E, the sets Exp_{2}(E) and Exp_{3}(E) of time expressions of E are defined as follows:

\begin{matrix}Exp_{2}(δ) = ∅ & Exp_{3}((e)E) = Exp_{1}((e)E) ∪ Exp_{2}(E) \\ Exp_{3}(δ) = ∅ & Exp_{2}(a(t)_{e}^{e′}. E) = Exp_{3}(E) \\ Exp_{2}(nil) = ∅ & Exp_{3}(a(t)_{e}^{e′}. E) = Exp_{1}(a(t)_{e}^{e′}. E) ∪ Exp_{3}(E) \\ Exp_{3}(nil) = ∅ & Exp_{2}(E + F) = Exp_{2}(E) ∪ Exp_{2}(F) \\ Exp_{2}((e)E) = Exp_{2}(E) & Exp_{3}(E + F) = Exp_{3}(E) ∪ Exp_{3}(F) \end{matrix}

Proposition 6.3.8 For any normal form E, where E ≡ ∑_{i∈I} a_{i}(t_{i})_{e_{i}}^{e′_{i}}. E_{i} + (e)δ, we have

Exp_{3}(E) = ⋃_{i∈I} Exp_{3}(E_{i}) ∪ {e + 0, e_{i}, e′_{i} : i ∈ I}

Proof: Straightforward. □

For any set S of time expressions, let Basic(S) be the set of time expressions resulted by eliminating max and min in S by the following procedure:

1 Let Basic(S) be S.

2 If max(e, f) ∈ Basic(S) or min(e, f) ∈ Basic(S), then replace max(e, f) or min(e, f) by e and f in Basic(S).

3 If e∘max(f, f′) ∈ Basic(S), or max(f, f′)∘e ∈ Basic(S), replace them by e∘f and e ∘ f′, where ∘ is + or ˙−.

4 If e ∘ min(f, f′) ∈ Basic(S), or min(f, f′) ∘ e ∈ Basic(S), replace them by e ∘ f and e ∘ f′, where ∘ is + or ˙−.

5 Repeat steps 2 to 4 until there is no occurrence of min or max in Basic(S).

For any set S of time expressions, we say S only contains time expressions which have single occurrence of the same time variables if for any time expression e of Basic(S) and any time variable t, if t occurs in e, then e satisfies one of the following conditions:

(1) e = f ∘ t or e = t ∘ f for some time expression f, where t ∉ fv(f), and ∘ is + or ˙−.

(2) e = e_{1} ∘ e_{2} for some time expressions e_{1} and e_{2} such that t ∉ fv(e_{2}) and e_{1} satisfies one of the two conditions, or t ∉ fv(e_{1}) and e_{2} satisfies one of the two conditions, where ∘ is + or ˙−.

Let E′ be the set of all processes such that for any E ∈ E′, Basic(Exp_{3}(E)) only contains time expressions which have single occurrence of the same time variables. The sublanguage of E′ is still very rich. In fact, we have the following property:

Proposition 6.3.9 For any processes E and F, if E, F ∈ E′ , then E + F is still in E′. Also if {e, e′} only contains time expressions which have single occurrence of the same time variables and E ∈ E′, then α(t)_{e}^{e′}. E ∈ E′.

Proof: Note that Basic(Exp_{3}(E + F)) = Basic(Exp_{3}(E)) ∪ Basic(Exp_{3}(F)) and Basic(Exp_{3}(α(t)_{e}^{e′}. E)) = Basic({e, e′}) ∪ Basic(Exp_{3}(E)). The result is straightforward. □

Remark If we consider the language defined by the syntax of Chapter 3, we only need to restrict the definition of time expressions such that the new definition of time expressions only allows those time expressions which have single occurrence of the same time variables, i.e. we only allow time expressions defined by the following:

1. for any u ∈ T and t ∈ V_{t}, u and t are time expressions;

2. for any time expression e and time variable t ∈ V_{t}, if t does not occur in e, then e + t, t + e, e ˙−t, t ˙−e, max(e, t), max(t, e), min(e, t) and min(t, e) are all time expressions. □

Now we can show that for the processes of E′, Lemma 6.3.2 of the last section still holds.

Lemma 6.3.10 For any processes E and F, where E ∈ E′ and F ∈ E′, W C(E, F) can be written in the disjunctive normal form

⋁_{i∈I} e_{1i} ≤ t_{1} ≤ f_{1i} ∧ ⋯ ∧ e_{ni}(t_{1}, …, t_{n−1}) ≤ t_{n} ≤ f_{ni}(t_{1}, …, t_{n−1})

for some n and I, where I is finite, and e_{ki}(t_{1}, …, t_{k−1}), f_{ki}(t_{1}, …, t_{k−1}) (k = 1, ⋯, n) contain at most variables t_{1}, …, t_{k−1}.

Proof: The proof is similar to that of Lemma 6.3.2 (note the restriction over occurrences of time variables in time expressions). □

Proposition 6.3.11 For any processes E and F, where E ∈ E′ and F ∈ E′ are in normal form, W C(E, F) ⊢ E = F.

Proof: Analogous to Proposition 6.3.3. □

By Lemma 6.3.1 and Proposition 6.3.11, the following results are straightforward.

Corollary 6.3.12 For any processes E ∈ E′ and F ∈ E′, A ⊧ E ∼ F implies A ⊢ E = F.

Corollary 6.3.13 (Completeness) For any processes E and F of E′,

E ∼ F implies ⊢ E = F

Remark Although it is not known if the above relativised compositional proof system is complete for general processes over discrete time domains, the simple proof system discussed in the begining of the chapter is complete over discrete time domains.

6.4 Proofs of Recursively Defined Processes

In this section, we consider the proofs of recursively defined processes. We show by an example how the proof system works for recursively defined processes. To do so, the proof system needs to be augmented with an axiom

true ⊢ μX.E = E{μX.E/X}

and some form of induction. We choose a very simple form of induction, namely Unique Fixpoint Induction:

true ⊢ P = E{P/X}
true ⊢ P = μX.E

The soundness of the axiom follows from Proposition 4.3.5. For a weakly guarded process E, the soundness of the above inductive rule follows from Proposition 4.3.5 and Corollary 4.5.5. However the inductive rule, in general, is not valid for processes which are not weakly guarded. For example, if E ≡ X, then for any process P we have P ∼ X{P/X} and clearly a(t)_{0}^{10}. nil ≁ μX.X. Also, for every agent P, we have P + a(t)_{0}^{10}. δ ∼ (a(t)_{0}^{10}. δ + X){(P + a(t)_{0}^{10}. δ)/X}, but P + a(t)_{0}^{10}. δ ≁ μX.a(t)_{0}^{10}. δ + X when we have P ≡ b(s)_{0}^{10}. δ.

Now we consider processes

P ≡ μX.a(t)_{1}^{10}. (b(s)_{0}^{t−(2 ˙−t)}. X + b(s)_{0}^{2t−2}. X + b(s)_{0}^{t}. X)

and

Q ≡ μX.a(t)_{1}^{10}. (b(s)_{0}^{2t−2}. X + b(s)_{0}^{t}. X)

We show how to derive

⊢ P = Q

in the extended proof system.

Chapter 6. A Proof System 109

Since Q is recursively defined and weakly guarded, by the above induction rule we only need to show that

⊢ P = a(t)_{1}^{10}. (b(s)_{0}^{2t−2}. P + b(s)_{0}^{t}. P)

However we have

⊢ P = a(t)_{1}^{10}. (b(s)_{0}^{t−(2 ˙−t)}. P + b(s)_{0}^{2t−2}. P + b(s)_{0}^{t}. P)

By rule 1 we only need to show ⊢ a(t)_{1}^{10}. (b(s)_{0}^{t−(2 ˙−t)}. P + b(s)_{0}^{2t−2}. P + b(s)_{0}^{t}. P) = a(t)_{1}^{10}. (b(s)_{0}^{2t−2}. P + b(s)_{0}^{t}. P) Clearly

⊢ P = P
⊢ b(s)_{0}^{2t−2}. P = b(s)_{0}^{2t−2}. P

and

⊢ b(s)_{0}^{t}. P = b(s)_{0}^{t}. P

By rule 5, we have

t ≥ 2 ⊢ b(s)_{0}^{t−(2 ˙−t)}. P = b(s)_{0}^{t}. P

and

t ≤ 2 ⊢ b(s)_{0}^{t−(2 ˙−t)}. P = b(s)_{0}^{2t−2}. P

By rule 7, we have t ≤ 2 ∨ t ≥ 2 ⊢ b(s)_{0}^{t−(2 ˙−t)}. P + b(s)_{0}^{2t−2}. P + b(s)_{0}^{t}. P = b(s)_{0}^{2t−2}. P + b(s)_{0}^{t}. P Since 1 ≤ t ≤ 10 → t ≤ 2 ⋁ t ≥ 2, by rule 3 we have 1 ≤ t ≤ 10 ⊢ b(s)_{0}^{t−(2 ˙−t)}. P + b(s)_{0}^{2t−2}. P + b(s)_{0}^{t}. P = b(s)_{0}^{2t−2}. P + b(s)_{0}^{t}. P By rule 5, we have the result ⊢ a(t)_{1}^{10}. (b(s)_{0}^{t−(2 ˙−t)}. P + b(s)_{0}^{2t−2}. P + b(s)_{0}^{t}. P) = a(t)_{1}^{10}. (b(s)_{0}^{2t−2}. P + b(s)_{0}^{t}. P)

Remark Even untimed CCS is Turing-powerful [Mil89a] and therefore no effective complete proof system can exist. By adding sufficiently powerful inductive methods for handling recursively defined processes, we would have a complete (and therefore ineffective) proof system for reasoning about real-timed processes.

6.5 Conclusion

In this chapter, we proposed a simple proof system for strong equivalence. The proof system is independent of the choice of time domain, allowing time to be discrete or dense. We showed the soundness of the proof system. We also showed that the proof system is complete for finite processes over dense time domains, but only complete for processes of a restricted language over discrete time domains. We discussed how to restrict the definition of time expressions to get the restricted language. There are no infinitary proof rules and the proof system is realistic and hopefully useful.

Although the proof system is presented for Timed CCS, the approach can also be used for other work. For example, the approach can be used for the restricted language of Baeten and Bergstra’s ACP ρI discussed in [Klu91] (restricting to those prefixed integrations and not allowing general integration). As discussed in Chapter 3, the restricted language of ACP ρI corresponds to Timed CCS.

Recently, Klusener proposed a sound and complete proof system [Klu91] for finite processes of the restricted language of ACP ρI and the work is for absolute time. In [Che91a], the author presents a sound and complete proof system (for finite processes) for relative time. The work of [Che91a,Klu91] is based on some powerful infinitary rules. If in Timed CCS, such an infinitary rule would be

∀u(e ≤ u ≤ e′), E{u/t} = F {u/t}

α(t)_{e}^{e′}. E = α(t)_{e}^{e′}. F

The presence of infinitary rules means that the proof systems, although sound and complete, are only of theoretical interest.

Behavioural Abstraction in Timed Processes

Strong bisimulation does not consider the problem of abstraction. It deals with the internal action τ in the same way as all other actions and requires that every τ action in one agent to be matched by a τ action of the other. In this chapter, we define some weak equivalences which abstract away the internal actions.

7.1 Weak Bisimulation

We first define a weak bisimulation which allows every internal action τ to be matched by zero or more τ actions.

Since the internal action τ is not observable, an agent which performs some τ actions during time u cannot be distinguished from an agent which just idles time u without any action, including τ actions. We define a transition P ⟹^{ϵ}_{u}P′ which means that agent P idles time u without any observable actions. So P ⟹^{ϵ}_{u}P′ may involve internal silent transitions. For convenience, we also write P ⟹_{u}P′ in

place of P ⟹^{ϵ}_{u}P′.

Definition 7.1.1 We say P ⟹^{ϵ}_{v+u_{1}+···+u_{n}}P′ if P ⟶^{τ}_{u_{1}} ⋯ ⟶^{τ}_{u_{n}} ·⟶_{v}P′ for some

u_{1}, …, u_{n}, v ∈ T . In particular, P ⟹^{ϵ}_{0}P.

We also define a transition P ⟹^{a}_{u}P′ which means that an action a is observed at time u. However, before action a, there may be finitely many unobservable internal actions, i.e. τ actions. Also there may be finitely many internal actions happening at the same time as action a (we say two actions happen at the same time if one follows another without any delay between them).

Definition 7.1.2 We say P ⟹^{a}_{u+v}P′ if P ⟹^{ϵ}_{u} · ⟶^{a}_{v} · ⟹^{ϵ}_{0}P′ for some u, v ∈ T .

Notation α̂ =^{def} if α = τ then ϵ else α. □

Definition 7.1.3 A binary relation R ⊆ P ×P is a weak bisimulation if (P, Q) ∈ R implies that for any α ∈ Act and u ∈ T

1 if P ⟹^{α}_{u}P′, then Q⟹^{α̂}_{u}Q′ and (P′, Q′) ∈ R for some Q′;

2 if P ⟶_{u}P′, then Q⟹^{ϵ}_{u}Q′ and (P′, Q′) ∈ R for some Q′;

3 if Q⟹^{α}_{u}Q′, then P ⟹^{α̂}_{u}P′ and (P′, Q′) ∈ R for some P′; and

4 if Q⟶_{u}Q′, then P ⟹^{ϵ}_{u}P′ and (P′, Q′) ∈ R for some P′.

Remark If we replace transitions of the form P ⟹^{α}_{u}P′ by transitions of the form P ⟶^{α}_{u}P′, we get the same weak bisimulations.

We say two agents P and Q are weakly bisimilar if there is a weak bisimulation R such that (P, Q) ∈ R.

Definition 7.1.4 ≈ = ⋃{R : R is a weak bisimulation}

Proposition 7.1.5 ≈ is the largest weak bisimulation. Moreover it is an equivalence relation.

Proof: The proof follows from the facts that the union, the composition and the inverse of weak bisimulations are still weak bisimulations and also the identity relation over agents is a weak bisimulation. □

Clearly, for any agents P and Q, P ≈ Q and P ⟹^{ϵ}_{t}P′ implies that Q⟹^{ϵ}_{t}Q′ and P′ ≈ Q′ for some Q′.

Definition 7.1.6 We say S is a weak bisimulation up to ≈ if P SQ implies that

(1) if P ⟹^{α}_{u}P′, then Q⟹^{α̂}_{u}Q′ and P′ ≈ ·S· ≈ Q′ for some Q′;

(2) if P ⟶_{u}P′, then Q⟹_{u}Q′ and P′ ≈ ·S· ≈ Q′ for some Q′;

(3) if Q⟹^{α}_{u}Q′, then P ⟹^{α̂}_{u}P′ and P′ ≈ ·S· ≈ Q′ for some P′; and

(4) if Q⟶_{u}Q′, then P ⟹_{u}P′ and P′ ≈ ·S· ≈ Q′ for some P′.

Similarly to strong bisimulation, we show that, to establish P ≈ Q, it is enough to show that there is a weak bisimulation up to ≈ which contains the pair (P, Q).

Proposition 7.1.7 If S is a weak bisimulation up to ≈, then S ⊆≈.

Proof: Analogous to Proposition 4.1.9. □

Remark If we use transitions of the form P ⟶^{α}_{t}P′ to replace the transitions of the form P ⟹^{α}_{t}P′ in Definition 7.1.3, then the proposition does not hold [SM92]. □

A strong bisimulation is also a weak bisimulation, as shown by the following proposition:

Proposition 7.1.8 If P ∼ Q, then P ≈ Q.

Proof: Straightforward. □

All laws for strong equivalence still hold for weak equivalence. Moreover, we have some properties which distinguish ≈ from ∼. As a result, strong equivalence has more discriminating power than weak bisimulation.

Proposition 7.1.9

(1) Q + τ(t)_{u}^{u′}. (t >> (u)P) + (u)P ≈ Q + τ(t)_{u}^{u′}. (t >> (u)P)

where | Q |_{T} ≤ u ≤ u′

(2) τ(t)_{u}^{u′}. (t >> ((u)P + (u′)δ)) ≈ (u)P + (u′)δ where u ≤ u′

(3) Q+τ(t)_{u}^{u′}. (t >> ((u)P +(u′)δ)) ≈ Q+(u)P +(u′)δ where | Q |_{T} < u ≤ u′

Proof: All properties may be proved by exhibiting appropriate weak bisimulations. We only consider (2), as all others are similar.

For (2), it is enough to show that

S = {(τ(t)_{v}^{v′}. (t >> ((v)P + (v′)δ)), (v)P + (v′)δ) : 0 ≤ v ≤ v′} ∪ ≈

is a weak bisimulation up to ≈.

- Suppose τ(t)_{v}^{v′}. (t >> ((v)P + (v′)δ))⟹^{α}_{u}P′. If α = τ, then for some w, where

v ≤ w ≤ v′ and w ≤ u, τ(t)_{v}^{v′}. (t >> ((v)P + (v′)δ))⟶^{τ}_{w}w >> ((v)P + (v′)δ)

and w >> ((v)P + (v′)δ)⟹^{ϵ}_{u−w}P′. Clearly (v)P + (v′)δ⟶_{w}Q for some Q such that Q ∼ w >> ((v)P + (v′)δ). So (v)P + (v′)δ⟹^{ϵ}_{u}Q′ for some Q′ such that P′ ≈ Q′. If α ≠ τ, then for some w, where v ≤ w ≤ v′

and w ≤ u, τ(t)_{v}^{v′}. (t >> ((v)P + (v′)δ))⟶^{τ}_{w}w >> ((v)P + (v′)δ) and

w >> ((v)P + (v′)δ)⟹^{α}_{u−w}P′. However (v)P + (v′)δ⟶_{w}Q for some Q,

where Q ∼ w >> ((v)P + (v′)δ)⟹^{α}_{u−w}P′. So (v)P + (v′)δ⟹^{α}_{w}Q′ for some

Q′ such that P′ ≈ Q′.

- Suppose τ(t)_{v}^{v′}. (t >> ((v)P + (v′)δ))⟶_{u}P′. Then u ≤ v′ and P′ ≡ τ(t)_{v ˙−u}^{v′−u}. (t + u >> ((v)P + (v′)δ)). If u ≤ v, then

P′ ≈ τ(t)_{v−u}^{v′−u}. (t >> ((v − u)P + (v′ − u)δ))

and (v)P +(v′)δ⟶_{u}P′′ for some P′′, where P′′ ∼ (v−u)P +(v′−u)δ. Clearly P′ ≈ ·S· ≈ P′′. If u ≥ v, then P′ ≈ τ(t)_{0}^{v′−u}. (t >> (u − v >> P + (v′ − u)δ) and (v)P + (v′)δ⟶_{u}P′′ for some P′′, where P′′ ∼ u − v >> P + (v′ − u)δ. Clearly P′ ≈ ·S· ≈ P′′.

- Suppose (v)P +(v′)δ)⟹^{α}_{u}P′. Then (v)P ⟹^{α}_{u}P′ and u ≥ v. Clearly τ(t)_{v}^{v′}. (t >>

((v)P + (v′)δ))⟶^{τ}_{v}⟶^{α}_{u−v}P′′ for some P′′ such that P′′ ≈ P′.

- Suppose (v)P + (v′)δ)⟶_{u}P′.

Case 1 u ≤ v, then P′ ≈ (v − u)P + (v′ − u)δ. Clearly τ(t)_{v}^{v′}. (t > > ((v)P +(v′)δ))⟶_{u}τ(t)_{v−u}^{v′−u}. (t+u >> ((v)P +(v′)δ)) where τ(t)_{v−u}^{v′−u}. (t+ u >> ((v)P + (v′)δ)) ≈ τ(t)_{v−u}^{v′−u}. (t >> ((v − u)P + (v′ − u)δ)). So

P′ ≈ ·S· ≈ τ(t)_{v−u}^{v′−u}. (t + u >> ((v)P + (v′)δ)).

Case 2 v < u ≤ v′, then P′ ∼ u − v >> P + (v′ − u)δ. Clearly τ(t)_{v}^{v′}. (t >> ((v)P +(v′)δ))⟶_{u}τ(t)_{0}^{v′−u}. (t+u >> ((v)P +(v′)δ)) where τ(t)_{0}^{v′−u}. (t+ u >> ((v)P + (v′)δ)) ≈ τ(t)_{0}^{v′−u}. (t >> (u − v >> P + (v′ − u)δ)). So

P′ ≈ ·S· ≈ τ(t)_{0}^{v′−u}. (t + u >> ((v)P + (v′)δ))

Case 3 v′ < u, then P′ ∼ u − v′ >> P. Clearly τ(t)_{v}^{v′}. (t >> ((v)P +

(v′)δ))⟶^{τ}_{v′}⟶_{u−v′}P′′ for some P′′, where P′′ ∼ u − v′ >> P. So

P′ ≈ P′′.

All other cases are straightforward. □

Note that the side conditions in Proposition 7.1.9 are important, as seen by the following counterexamples:

- for (1), we have a(t)_{0}^{10}. δ +τ(s)_{0}^{5}. (s >> b(r)_{1}^{10}. δ)+b(r)_{1}^{10}. δ ≉ a(t)_{0}^{10}. δ +τ(s)_{0}^{5}. (s >> b(r)_{1}^{10}. δ), where the left hand side delays 10 seconds (if time is measured in seconds) and then evolves to a state which can perform either action a or action b but the right hand side can only either do action a or do action b (without choice) after a delay of 10 seconds without any observable actions;

- for (2), we have τ(t)_{8}^{6}. (t >> a(s)_{10}^{15}. δ) + a(s)_{10}^{15}. δ ≉ τ(t)_{8}^{6}. (t >> a(s)_{10}^{15}. δ) as the left hand side can perform action a at time 10 which is not matched by right hand side; and

- for (3), we have a(t)_{0}^{10}. δ +τ(s)_{8}^{15}. (s >> (8)b(r)_{0}^{10}. δ) ≉ a(t)_{0}^{10}. δ +(8)b(r)_{0}^{10}. δ, where the left hand side can have an internal transition at 10 seconds and then can only perform action b but the right hand side can always do either action a or action b after a delay of 10 seconds without any observable actions.

Similarly to CCS, weak equivalence is not a congruence relation. In general the summation operation does not preserve weak equivalence. For example, τ(t)_{2}^{8}. nil ≈ nil, but τ(t)_{2}^{8}. nil + a(s)_{8}^{∞}. nil ≉ nil + a(s)_{8}^{∞}. nil. However, weak equivalence is preserved by the other operations.

Proposition 7.1.10 For any agents P and Q, P ≈ Q implies

\begin{matrix}(1) α(t)_{e}^{e′}. P ≈ α(t)_{e}^{e′}. Q & (3) P \a ≈ Q\a \\ (2) P | R ≈ Q | R & (4) P [S] ≈ Q[S] \end{matrix}

Proof: All properties may be proved by exhibiting appropriate weak bisimulations. We only consider (2), as all other cases are similar.

For (2), we only need to show that the relation

S = {(P | R, Q | R) : P ≈ Q}

is a weak bisimulation. □

As for strong bisimulation, we can also generalize the definition of weak bisimulation to any processes.

Definition 7.1.11 For any processes E and F which are closed with respect to process variables and contain at most free time variables t⃗ = (t_{1}, …, t_{n}), we say E ≈ F if for any u⃗ ∈ T^{n} we have E{u⃗/t⃗} ≈ F {u⃗/t⃗}.

Definition 7.1.12 For any processes E and F which contain at most free process variables X⃗ = (X_{1}, …, X_{n}), we say E ≈ F if for any agents P⃗ = (P_{1}, …, P_{n}), we have E{P⃗ /X⃗} ≈ F {P⃗ /X⃗}.

All properties for agents also hold for processes. For example, for any processes E and F, if E ∼ F, then E ≈ F.

7.2 Observational Congruence

Weak equivalence is not fully substitutive. In general, it is not preserved by summation operator. In this section, we define an equality which will be fully substitutive and also the largest congruence relation included in ≈. The following definition for =^{+} is a standard CCS technique.

Definition 7.2.1 We say E =^{+} F if for any agent P, we have E + P ≈ F + P.

Clearly =^{+} is included in ≈. In fact =^{+} lies between the strong and the weak equivalences.

Proposition 7.2.2 E ∼ F implies E =^{+} F and E =^{+} F implies E ≈ F.

Proof: The first part follows from the facts that strong equivalence is preserved by summation and E ∼ F implies E ≈ F. The second part follows by taking P ≡ δ in the definition of =^{+}. □

The converse of the above does not hold. For example, τ.nil ≈ nil, but τ.nil ≠^{+} nil. Also a(t)_{2}^{10}. τ.nil =^{+} a(t)_{2}^{10}. nil, but a(t)_{2}^{10}. τ.nil ≁ a(t)_{2}^{10}. nil.

We say an agent is stable if it cannot perform an internal action τ as its first action.

Definition 7.2.3 An agent P is stable if there are no P′ or u ∈ T such that

P ⟶^{τ}_{u} P′.

Proposition 7.2.4 For any stable agents P and Q, P ≈ Q implies P =^{+} Q

Proof: We only need to show that the relation

S = {(P + R, Q + R) : P ≈ Q & both P and Q are stable}∪ ≈

is a weak bisimulation.

The case (P, Q) ∈≈ is trivial. Now we consider the case (P + R, Q + R) ∈ S for any agents P, Q and R, where P and Q are stable and satisfy P ≈ Q.

- if P + R⟹^{α}_{u}P′, then P ⟹^{α}_{u}P′ or R⟹^{α}_{u}P′.

Case 1 P ⟹^{α}_{u}P′, then α ≠ τ (P is stable). So Q⟹^{α}_{u}Q′ and P′ ≈ Q′ for

some Q′. Hence Q + R⟹^{α}_{u}Q′ and P′ ≈ Q′.

Case 2 R⟹^{α}_{u}P′, then Q + R⟹^{α}_{u}P′ and P′ ≈ P′.

- if P + R⟶_{u}P′′, then 0 ≤ u ≤ max( | P |_{T} , | R |_{T}).

Case 1 u ≤ min( | P |_{T} , | R |_{T}), then P ⟶_{u}P′, R⟶_{u}R′ and P′′ ≡ P′ + R′. Clearly P′ is still stable. So Q⟶_{u}Q′ and P′ ≈ Q′ for some Q′ (Q is stable). Similarly Q′ is still stable. Hence Q + R⟶_{u}Q′ + R′ and (P′ + R′, Q′ + R′) ∈ S.

Case 2 | P |_{T} < u ≤ | R |_{T}, then R⟶_{u}P′. Since P, Q are stable and

P ≈ Q, we have Q + R⟶_{u}P′ and P′ ≈ P′.

Case 3 | R |_{T} < u ≤ | P |_{T}, then P ⟶_{u}P′. So Q⟶_{u}Q′ and P′ ≈ Q′ for

some Q′ (Q is stable). Hence Q + R⟶_{u}P′ and P′ ≈ P′.

By symmetry, we are done. □

Proposition 7.2.5 E ≈ F implies α(t)_{e}^{e′}. E =^{+} α(t)_{e}^{e′}. F.

Proof: We only need to consider the case that α(t)_{e}^{e′}. E and α(t)_{e}^{e′}. F are agents. If α ≠ τ, the result follows from Lemma 7.1.10 and Lemma 7.2.4. Now suppose α = τ. It is enough to show that the relation

S = {(τ(t)_{v}^{v′}. E + R, τ(t)_{v}^{v′}. F + R) : E ≈ F & fv_{t}(E, F) ⊆ {t} & fv_{p}(E, F) = ∅}∪ ≈

is a weak bisimulation.

The case (P, Q) ∈≈ is trivial. Now we consider the case (τ(t)_{v}^{v′}. E+R, τ(t)_{v}^{v′}. F + R) ∈ S for any agents τ(t)_{v}^{v′}. E, τ(t)_{v}^{v′}. F and R, where E ≈ F.

- if τ(t)_{v}^{v′}. E + R⟹^{α}_{u}P, then τ(t)_{v}^{v′}. E⟹^{α}_{u}P or R⟹^{α}_{u}P.

Case 1 τ(t)_{v}^{v′}. E⟹^{α}_{u}P, then α = τ and P ≡ E{u/t} or E{w/t}⟹^{α}_{u−w}P

for some w, where v ≤ w ≤ min(v′, u). In the first case, we have

τ(t)_{v}^{v′}. F + R⟶^{τ}_{u}F {u/t} and E{u/t} ≈ F {u/t}. In the second case, we

have F {w/t}⟹^{α̂}_{u−w}Q for some Q such that P ≈ Q.

Case 2 R⟹^{α}_{u}P, then τ(t)_{v}^{v′}. F + R⟹^{α̂}_{u}P and P ≈ P.

- if τ(t)_{v}^{v′}. E + R⟶_{u}P, then u ≤ max(v′, | R |_{T}).

Case 1 u ≤ min(v′, | R |_{T}), then P ≡ τ(t)_{v ˙−u}^{v′−u}. (E{u + t/t}) + R′ where R⟶_{u}R′. Clearly τ(t)_{v}^{v′}. F +R⟶_{u}τ(t)_{v ˙−u}^{v′−u}. (F {u+t/t})+R′ and E{u+

t/t} ≈ F {u + t/t}. So
(τ(t)_{v ˙−u}^{v′−u}. (E{u + t/t}) + R′, τ(t)_{v ˙−u}^{v′−u}. (F {u + t/t}) + R) ∈ S

Chapter 7. Behavioural Abstraction in Timed Processes 120

Case 2 v′ < u ≤ | R |_{T}, then R⟶_{u}P′. Clearly τ(t)_{v}^{v′}. F + R⟶_{u}P′ and

P′ ≈ P′.

Case 3 | R |_{T} < u ≤ v′, then P ≡ τ(t)_{v ˙−u}^{v′−u}. (E{u+t/t}). Clearly τ(t)_{v}^{v′}. F +

R⟶_{u}τ(t)_{v ˙−u}^{v′−u}. (F {u + t/t}) and
τ(t)_{v ˙−u}^{v′−u}. (E{u + t/t}) ≈ τ(t)_{v ˙−u}^{v′−u}. (F {u + t/t})

By symmetry, we are done. □ Proposition 7.2.6 (τ-Laws) 1 τ(t)_{0}^{e′}. (α.E + F) =^{+} α.(E{0/t}) + τ(t)_{0}^{e′}. (α.E + F) 2 α(t)_{e}^{e′}. (τ.E + F) =^{+} α(t)_{e}^{e′}. E + α(t)_{e}^{e′}. (τ.E + F) 3 α(t)_{f}^{f′}. (F + τ(s)_{e}^{e′}. (s >> (e)E) + (e)E) =^{+} α(t)_{f}^{f′}. (F + τ(s)_{e}^{e′}. (s >> (e)E))

where | F |_{T} ≤ e ≤ e′ & s ∉ fv_{t}(E)

4 α(t)_{f}^{f′}. (τ(s)_{e}^{e′}. (s >> ((e)E + (e′)δ))) =^{+} α(t)_{f}^{f′}. ((e)E + (e′)δ)

where e ≤ e′ & s ∉ fv_{t}((e)E + (e′)δ)

5 α(t)_{f}^{f′}. (F + τ(s)_{e}^{e′}. (s >> ((e)E + (e′)δ))) =^{+} α(t)_{f}^{f′}. (F + (e)E + (e′)δ)

where | F |_{T} < e ≤ e′ & s ∉ fv_{t}((e)E + (e′)δ)

Proof: Properties (3), (4) and (5) follow from Lemma 7.1.9 and Lemma 7.2.5. Properties (1) and (2) may be proved by showing appropriate weak bisimulations. We only consider (2), as (1) is similar.

For (2), it is enough to consider agents and show that the relation

S = {(α(t)_{v}^{v′}. (τ.E + F) + R, α(t)_{v}^{v′}. E + α(t)_{v}^{v′}. (τ.E + F) + R)

: fv_{t}(E) ⊆ {t} & fv_{p}(E) = ∅ & fv_{t}(F) ⊆ {t} & fv_{p}(F) = ∅}∪ ≈

is a weak bisimulation.

Chapter 7. Behavioural Abstraction in Timed Processes 121

- if α(t)_{v}^{v′}. E + α(t)_{v}^{v′}. (τ.E + F) + R⟹^{β}_{u}P

Case 1 α(t)_{v}^{v′}. E⟹^{β}_{u}P, then α(t)_{v}^{v′}. E⟶^{β}_{u}P and P ≡ E{u/t}, or α = τ and

E{w/t}⟹^{β}_{u−w}P for some w, where v ≤ w ≤ min(v′, u). In the first case, we have

α(t)_{v}^{v′}. (τ.E + F) + R⟶^{α}_{u}⟶^{τ}_{0}E{u/t}

In the second case, we have

α(t)_{v}^{v′}. (τ.E + F) + R⟶^{τ}_{w}⟶^{τ}_{0}E{w/t}

where v ≤ w ≤ min(v′, u) and E{w/t}⟹^{β}_{u−w}P.

Case 2 α(t)_{v}^{v′}. (τ.E + F)⟹^{β}_{u}P or R⟹^{β}_{u}P, straightforward.

- if α(t)_{v}^{v′}. E + α(t)_{v}^{v′}. (τ.E + F) + R⟶_{u}P, then u ≤ max(v′, | R |_{T}).

Case 1 u ≤ min(v′, | R |_{T}), then

P ≡ α(t)_{v ˙−u}^{v′−u}. (E{t + u/t}) + α(t)_{v ˙−u}^{v′−u}. (τ.E + F){t + u/t} + R′ where R⟶_{u}R′. Clearly

α(t)_{v}^{v′}. (τ.E + F) + R⟶_{u}α(t)_{v ˙−u}^{v′−u}. (τ.E + F){t + u/t} + R′ and

(α(t)_{v ˙−u}^{v′−u}. (τ.E + F){t + u/t} + R′, P) ∈ S

Case 2 v′ < u ≤ | R |_{T}, then R⟶_{u}P. Clearly

α(t)_{v}^{v′}. (τ.E + F) + R⟶_{u}P

Case 3 | R |_{T} < u ≤ v′, then P ≡ α(t)_{v ˙−u}^{v′−u}. (E{t + u/t}) + α(t)_{v ˙−u}^{v′−u}. (τ.E + F){t + u/t} Clearly

α(t)_{v}^{v′}. (τ.E + F) + R⟶_{u}α(t)_{v ˙−u}^{v′−u}. (τ.E + F){t + u/t})

and

(α(t)_{v ˙−u}^{v′−u}. (τ.E + F){t + u/t}, P) ∈ S

All other cases are straightforward. □

We can also give an alternative definition of =^{+} via the transitions ⟶_{u}, ⟶^{α}_{0} and ⟹^{α}_{0}. To do so, we first define an equivalence =^{c} and then show that =^{+} and =^{c} coincide.

Definition 7.2.7 A binary relation R over agents is a C-bisimulation if (P, Q) ∈ R implies that for any α ∈ Act and u ∈ T ,

(1) if P ⟶^{α}_{0}P′, then Q⟹^{α}_{0}Q′ and P′ ≈ Q′ for some Q′;

(2) if P ⟶_{u}P′, then Q⟶_{u}Q′ and (P′, Q′) ∈ R;

(3) if Q⟶^{α}_{0}Q′, then P ⟹^{α}_{0}P′ and P′ ≈ Q′ for some P′; and

(4) if Q⟶_{u}Q′, then P ⟶_{u}P′ and (P′, Q′) ∈ R.

Definition 7.2.8 =^{c} =^{def} ⋃{R : R is a C-bisimulation}.

Proposition 7.2.9 For any weakly guarded agents P and Q, P =^{c} Q if and only if P =^{+} Q.

Proof: (⇒) It is enough to show that

S = {(P + R, Q + R) : P =^{c} Q}∪ ≈

is a weak bisimulation.

The case of (P, Q) ∈≈ is trivial. We only consider here the case (P +R, Q+R) ∈ S for any agents P, Q and R, where P =^{c} Q.

- if P + R⟹^{α}_{u}P′

Case 1 P ⟹^{α}_{u}P′. If α ≠ τ, then Q⟹^{α}_{u}Q′ for some Q′ such that P′ ≈ Q′. Now suppose α = τ. Then P ⟶_{w}⟶^{τ}_{0}⟹^{ϵ}_{u−w}P′ for some w, where w ≤ u. Since P =^{c} Q, we have Q⟶_{w}⟹^{τ}_{0}⟹^{ϵ}_{u−w}Q′ for some Q′ such

that P′ ≈ Q′. So Q + R⟹^{α}_{u}Q′ and P′ ≈ Q′ for some Q′.

Case 2 R⟹^{α}_{u}P′, then Q + R⟹^{α}_{u}P′.

- if P + R⟶_{u}P′, then u ≤ max( | P |_{T} , | R |_{T}).

Case 1 u ≤ min( | P |_{T} , | R |_{T}), then P′ ≡ P′′ + R′ where P ⟶_{u}P′′ and R⟶_{u}R′. Clearly Q⟶_{u}Q′′ and P′′ =^{c} Q′′ for some Q′′. So Q +

R⟶_{u}Q′′ + R′ and (P′′ + R′, Q′′ + R′) ∈ S.

Case 2 | P |_{T} < u ≤ | R |_{T}, then R⟶_{u}P′. So Q + R⟶_{u}P′ and P′ ≈ P′.

Case 3 | R |_{T} < u ≤ | P |_{T}, then P ⟶_{u}P′. Clearly Q⟶_{u}Q′ and P′ =^{c} Q′ for some Q′. So Q + R⟶_{u}Q′. It is easy to check that P′ =^{c} Q′ implies

P′ ≈ Q′.

By symmetry, we are done.

(⇐) Suppose P ≠^{c} Q and for any a ∈ Act, u ∈ T

Case 1 P ⟶_{u} · ⟶^{α}_{0}P′, but whenever Q⟶_{u} · ⟹^{α}_{0}Q′ then P′ ≉ Q′.

We choose R ≡ ℓ(t)_{u}^{u}. nil, where ℓ is a fresh action which does not occur in P and Q. Since P + R⟶_{u} · ⟶^{α}_{0}P′, we show that whenever Q + R⟹_{u}⟹^{α}_{0}Q′ then P′ ≉ Q′. Clearly, ⟹_{u} ≡ ⟶_{u}, otherwise Q + R⟹_{u}Q′′, where Q⟹_{u}Q′′, and u >> (P + R) ≉ Q′′. If α = τ and Q′ ≡ u >> (Q + R), then P′ ≉ Q′ (Q′ may perform action ℓ). In all other cases, we have

Q + R⟶_{u} · ⟹^{α}_{0}Q′, where Q⟶_{u} · ⟹^{α}_{0}Q′, and P′ ≉ Q′. So we have

P ≠^{+} Q.

Case 2 P ⟶_{u}P′, but | Q |_{T} < u.

If P′ ≉ δ, then we choose a v, where | Q |_{T} < v ≤ u, and let R ≡ ℓ(t)_{v}^{v}. nil, where ℓ is a fresh action which does not occur in P and Q. Then P + R⟶_{v}v >> (P + R) is not matched by Q + R. Now suppose P′ ≈ δ. Let v = | Q |_{T} and R ≡ ℓ(t)_{v}^{v}. nil, where ℓ is a fresh action which does not occur in P and Q. If Q⟶^{τ}_{v}Q′, then Q + R⟶^{τ}_{v}Q′ is not matched by P + R. Otherwise P + R⟶_{v}P′′ + ℓ(t)_{0}^{0}. nil, where P ⟶_{v}P′′ and P′′transu − vP′, is not matched by Q + R. So we have P ≠^{+} Q.

By symmetry, we are done. □

Definition 7.2.10 We say S is a C-bisimulation up to =^{c} if P SQ implies that

(1) if P ⟶^{α}_{0}P′, then Q⟹^{α}_{0}Q′ and P′ ≈ Q′ for some Q′;

(2) if P ⟶_{u}P′, then Q⟶_{u}Q′ and P′ =^{c} S =^{c} Q′ for some Q′;

(3) if Q⟶^{α}_{0}Q′, then P ⟹^{α}_{0}P′ and P′ ≈ Q′ for some P′; and

(4) if Q⟶_{u}Q′, then P ⟶_{u}P′ and P′ =^{c} S =^{c} Q′ for some P′.

Proposition 7.2.11 If S is a C-bisimulation up to =^{c}, then S ⊆=^{c}.

Proof: Analogous to Proposition 4.1.9. □

Hence, to prove P =^{c} Q, we only need to find a C-bisimulation up to =^{c} which contains (P, Q).

Now we show that =^{+} is a congruence relation, i.e. it is substitutive for all operators including the recursive operator.

Proposition 7.2.12 E =^{+} F implies

(1) α(t)_{e}^{e′}. E =^{+} α(t)_{e}^{e′}. F  (4) E\a =^{+} F \a
(2) E + G =^{+} F + G  (5) E[S] =^{+} F [S]
(3) E | G =^{+} F | G

Proof: To prove (2), we only need to show that for every agent P, (E+G)+P ≈ (F + G) + P which follows from E =^{+} F. All other properties can be proved by exhibiting appropriate C-bisimulations. For example, for (3), we only need to show that the relation

S = {(P | R, Q | R) : P =^{c} Q}

is a C-bisimulation. □

Now we show that =^{+} is also preserved by recursive operator.

Proposition 7.2.13 For any processes E⃗ and F⃗ which contain at most process variables X⃗, E⃗ =^{+} F⃗ implies μX⃗.E⃗ =^{+} μX⃗.F⃗.

Proof: Analogous to Proposition 7.2.8 of [Mil89a]. □

7.3 Unique Solution of Equations

In this section, we show that under certain conditions the solutions of equations X⃗ = E⃗ are still unique up to observational congruence.

Definition 7.3.1 X is sequential in E if every subterm of E which contains X, apart from X itself, is of the form α(t)_{e}^{e′}. F or F_{1} + F_{2}.

Definition 7.3.2 X is guarded in E if every occurrence of X is within some subterm a(t)_{e}^{e′}. F of E, where a ≠ τ.

We say a process E is guarded (sequential) if all process variables of E are guarded (sequential) in E. Equations X⃗ = E⃗ are guarded (sequential) if all processes E⃗ are guarded (sequential). Similar to weak guardedness, the guardedness ensures that process variables cannot affect the first non-τ action.

Lemma 7.3.3 For any sequential process E and agents P⃗, if process variables X⃗ are guarded in E and E{P⃗ /X⃗}⟶^{α}_{u}P′, then there is a process H such that P′ ≡ H{P⃗ /X⃗} and for any agents Q⃗, we have E{Q⃗/X⃗}⟶^{α}_{u}H{Q⃗/X⃗}. Moreover H is also sequential and if α = τ, then H is still guarded.

Proof: Suppose E{P⃗ /X⃗}⟶^{α}_{u}P′. We proceed by induction on the structure of E. If E is a Recursion, a Composition, a Restriction or a Relabelling, then it contains no free process variables and the result is immediate (recall the definition of a sequential process). If E is a Summation, the result follows from induction.

If E ≡ α(t)_{v}^{v′}. F, then P′ ≡ F {P⃗ /X⃗}{u/t}, where v ≤ u ≤ v′. Since P⃗ are agents, F {P⃗ /X⃗}{u/t} ≡ F {u/t}{P⃗ /X⃗}. Also, for any agents Q⃗,

E{Q⃗/X⃗}⟶^{α}_{u}F {Q⃗/X⃗}{u/t} and F {Q⃗/X⃗}{u/t} ≡ F {u/t}{Q⃗/X⃗}

The result follows by taking H ≡ F {u/t}. Note that H must also be guarded if α = τ. □

Now we can show that for any guarded and sequential equations X⃗ = E⃗, where processes E⃗ contain at most free process variables X⃗, if the equations have solutions, then the solutions are unique up to observational congruence.

Proposition 7.3.4 Let E⃗ be guarded and sequential processes which are closed with respect to time variables and contain at most free process variables X⃗,

P⃗ =^{+} E⃗{P⃗ /X⃗} and Q⃗ =^{+} E⃗{Q⃗/X⃗} implies P⃗ =^{+} Q⃗

Proof: Analogous to Proposition 7.3.13 of [Mil89a]. □

Similarly to strong bisimulation, any guarded and sequential equations have solutions. As a result, any guarded and sequential equations have unique solution up to observational congruence.

Corollary 7.3.5 (Unique Solution) For any guarded and sequential equations X⃗ = E⃗, where E⃗ are closed with respect to time variables and contain at most free process variables X⃗, there is an unique solution P⃗ (up to observational congruence) such that

P⃗ =^{+} E⃗{P⃗ /X⃗}

7.4 Conclusion

In this section, we extended the notions of weak bisimulations and observational congruence to real-time processes. In [Cer92], it is shown that weak bisimulation for parallel networks of regular timed processes without time variables is decidable. However decidability and complete axiomatization problems of weak bisimulations for general finite processes (with time variables) are still open. It is not clear whether the techniques discussed in Chapter 5 and Chapter 6 can be used for weak bisimulations or observational congruence. As P ≈ Q in general does not imply τ(t)_{e}^{e′}. P =^{+} Q or P =^{+} τ(t)_{e}^{e′}. Q for some e and e′, this leaves the completeness problem hard.

Observing Causality in Real-Timed Calculi

CCS is a symbolic calculus, in the sense that it treats solely the observation of events of a system, and not their relative time, locations or duration. All these are abstracted away from consideration. For example, the term a.P in CCS represents the process which can perform an action a and evolve into the process P. The place, time and duration of the action a are not specified. The process is assumed to be idling for some amount of time before the action a occurs, and then some time later the new state P is reached. In this chapter we show that by specifying temporal aspects of processes, we can observe the usual notions of causality, concurrency and conflict within a system in the following sense:

• two events are causally related if they can both occur in the same run, but never at the same time. Here we make the assumption that a process a.P must delay by some nonzero time after the event a in order to stabilize.

• two events occur concurrently if they may occur at the same time.

• two events are conflicting if they cannot both occur in the same run.

With this observation, we show that we can develop an interleaving theory for CCS which respects these relationships, i.e. we develop an interleaving theory of a true concurrency semantics for CCS.

This chapter is joint work with Anderson and Moller and the work is still in progress [ACM92].

8.1 An Event Structure Semantics for CCS

We only treat here a simple language of finite terms which are defined by the following BNF expression.

P ::= nil | α.P | P + Q | P | Q

The results can be extended to the language with recursion and relabelling; their omission is only to facilitate an elegant presentation of the key ideas of the chapter.

In this section, we will propose an interpretation of CCS terms over labelled event structures, as presented in [BC89,DDM89].

Definition 8.1.1 Two labelled event structures E and F are isomorphic, written E ≅ F, if there exists a label-, order- and conflict-preserving bijection between them.

A semantics in terms of labelled event structures is still intensional, as in the case for the interleaving semantics based on synchronization trees. In [DDM89], the notion of partial order bisimulation on labelled event structures is defined.

Configurations of event structures can be regarded as special cases of event structures, with inherited concurrency, causality and conflict relations. As a result, we can define configuration isomorphism as the event structure isomorphism.

Definition 8.1.2 A configuration F′ of an event structure S is called an Sextension of the configuration F of S whenever F ⊆ F′.

Definition 8.1.3 A binary relation R over (event structure/configuration) pairs is a po-bisimulation if (S, E)R(T, F) implies E ≅ F and

1 if E′ is an S-extension of E, then there is an T -extension F′ of F such that (S, E′)R(T, F′); and

2 if F′ is an T -extension of F, then there is an S-extension E′ of E such that (S, E′)R(T, F′).

Two event structures S and T are po-bisimilar, written as S ∼_{P O} T, if ((S, ∅), (T, ∅)) ∈ R for some po-bisimulation R.

We may interpret a CCS term as an event structure using a mapping S, where the mapping S is inductively defined as following:

• S(nil) = (∅, ∅, ∅, ∅);

• If S(P) = (E, ≺, #, ℓ), then S(α.P) = (E ∪ {ε}, ≺′, #, ℓ′), where ε ∉ E and

– ≺′ = ≺ ∪ {(ε, e) : e ∈ E}
– ℓ′ = ℓ[ε ↦ α]

• If S(P_{i}) = (E_{i}, ≺_{i}, #_{i}, ℓ_{i}) for i = 0, 1, then S(P_{0} + P_{1}) = (E, ≺, #, ℓ) where

– E = E_{0} ⊎ E_{1}
– ≺ = ≺_{0} ⊎ ≺_{1}
– # = #_{0} ⊎ #_{1} ⊎ {(e_{0}, e_{1}), (e_{1}, e_{0}) : e_{i} ∈ E_{i}}
– ℓ = ℓ_{0} ⊎ ℓ_{1}

• If S(P_{i}) = (E_{i}, ≺_{i}, #_{i}, ℓ_{i}) for i = 0, 1, then S(P_{0} | P_{1}) = (E, ≺, #, ℓ) where

– E = E_{0} ⊎ E_{1} ⊎ \{(e_{0}, e_{1}) : e_{i} ∈ E_{i} & ℓ_{0}(e_{0}) = \overline{ℓ_{1}(e_{1})}\}

– ≺ = ≺_{0} ⊎ ≺_{1} ⊎ {(e_{j}, (e′_{0}, e′_{1})), ((e_{0}, e_{1}), e′_{j}) : e_{i}, e′_{i} ∈ E_{i} & e_{i} ≺_{i} e′_{i}}

⊎ {((e_{0}, e_{1}), (e′_{0}, e′_{1})) : e_{i}, e′_{i} ∈ E_{i} &
(e_{0} ≺_{0} e′_{0} ∨ e_{1} ≺_{1} e′_{1}) & ¬(e_{i}#e′_{i})}

– # = #_{0} ⊎ #_{1} ⊎ {(e_{j}, (e′_{0}, e′_{1})), ((e_{0}, e_{1}), e′_{j}) : e_{i}, e′_{i} ∈ E_{i} & e_{i}#_{i}e′_{i}}

⊎ {((e_{0}, e_{1}), (e′_{0}, e′_{1})) : e_{i}, e′_{i} ∈ E_{i} & (e_{0}#_{0}e′_{0} ∨ e_{1}#_{1}e′_{1})}
– ℓ = ℓ_{0} ⊎ ℓ_{1} ⊎ \{((e_{0}, e_{1}), τ ) : e_{i} ∈ E_{i} & ℓ_{0}(e_{0}) = \overline{ℓ_{1}(e_{1})}\}

Definition 8.1.4 For any CCS agents P and Q, we say P ∼_{P O} Q if S(P) ∼_{P O} S(Q).

Partial order bisimulation provides us with more discriminating power than interleaving bisimulation. As an example, we have

a | b ≁_{P O} a | b + ab

Compared with the pomset bisimulation of [BC87], partial order bisimulation also considers the (past) history of an actual step. As a result, partial order bisimulation has more discriminating power than pomset bisimulation. For example, we have

a | b + a(b + c) + ab ≁_{P O} a | b + a(b + c)

but pomset bisimulation cannot distinguish these two agents. As claimed in [DDM89] these agents should be differentiated whenever causal dependencies are important.

8.2 A Timed Semantics for CCS

In this section we interpret the symbolic calculus CCS within the loose temporal calculus ℓTCCS of [MT91], a sublanguage of the calculi TCCS of [MT90] and Timed CCS of Chapter 3.

Our model is an extension of CCS with real-time. Processes are defined by the following BNF expression, where t ranges over ^{+}, the positive reals. We let \underline{P}, \underline{Q} range over agents of ℓTCCS to avoid confusion with CCS agents. Also, the (delayed) nil and (delayed) action prefix operators of ℓTCCS are written with underscores.

\underline{P} ::= \underline{nil} | \underline{α}.\underline{P} |(t).\underline{P} | \underline{P} + \underline{Q} | \underline{P} | \underline{Q}

In Table 8–1, we present the operational rules for the language. The transitional semantics of the language is then given by the least relations

⟶ ⊆ ℓTCCS × Act × ℓTCCS and ⇝⊆ ℓTCCS × ^{+} × ℓTCCS

written as \underline{P}⟶^{α}\underline{Q} and \underline{P} ⇝^{t} \underline{Q} respectively, which satisfy the rules laid out in Figure 8–1. The rules for action derivations are identical to those in the calculus CCS. The only new feature is the temporal derivations.

Remark Although the time constants are taken from the positive reals, we allow ourselves to interpret (0).\underline{P} as syntactically identical to \underline{P}. Equally, we allow ourselves to write \underline{P} ⇝^{0} \underline{P}. □

Definition 8.2.1 We write \underline{P}⟶^{α}_{t}\underline{P}′ whenever \underline{P} ⇝^{t} ⟶^{α}\underline{P}′, and \underline{P} ⟶^{α_{1}···α_{n}}_{t_{1}+···+t_{n}} \underline{P}′ whenever \underline{P}⟶^{α_{1}}_{t_{1}} ⋯ ⟶^{α_{n}}_{t_{n}} \underline{P}′. In particular, \underline{P}\underrightarrow{ε}_{0}\underline{P}.

Definition 8.2.2 A binary relation R over ℓTCCS is a strong temporal bisimulation if (\underline{P}, \underline{Q}) ∈ R implies that for all α ∈ Act and t ∈ ^{+},

\overline{\underline{nil} ⇝^{t} \underline{nil}}  \overline{\underline{α}.\underline{P} ⇝^{t} \underline{α}.\underline{P}}

\overline{(s + t).\underline{P} ⇝^{s} (t).\underline{P}}  \overline{(t).\underline{P} ⇝^{t} \underline{P}}

\frac{\underline{P} ⇝^{s} \underline{P}′}{(t).\underline{P} ⇝^{s+t} \underline{P}′}

\frac{\underline{P} ⇝^{t} \underline{P}′, \underline{Q} ⇝^{t} \underline{Q}′}{\underline{P} + \underline{Q} ⇝^{t} \underline{P}′ + \underline{Q}′}

\frac{\underline{P} ⇝^{t} \underline{P}′, \underline{Q} ⇝^{t} \underline{Q}′}{\underline{P} | \underline{Q} ⇝^{t} \underline{P}′ | \underline{Q}′}

\overline{\underline{α}.\underline{P}⟶^{α}\underline{P}}  \frac{\underline{P}⟶^{α}\underline{P}′}{\underline{P} + \underline{Q}⟶^{α}\underline{P}′}

\frac{\underline{Q}⟶^{α}\underline{Q}′}{\underline{P} + \underline{Q}⟶^{α}\underline{Q}′}  \frac{\underline{P}⟶^{α}\underline{P}′}{\underline{P} | \underline{Q}⟶^{α}\underline{P}′ | \underline{Q}}

\frac{\underline{Q}⟶^{α}\underline{Q}′}{\underline{P} | \underline{Q}⟶^{α}\underline{P} | \underline{Q}′}

\frac{\underline{P}⟶^{a}\underline{P}′, \underline{Q}⟶^{ā}\underline{Q}′}{\underline{P} | \underline{Q}⟶^{τ}\underline{P}′ | \underline{Q}′}

Table 8–1: Operational Rules for ℓTCCS 1. if \underline{P}⟶^{α}_{t}\underline{P}′ then \underline{Q}⟶^{α}_{t}\underline{Q}′ for some \underline{Q}′ with (\underline{P}′, \underline{Q}′) ∈ R and

2. if \underline{Q}⟶^{α}_{t}\underline{Q}′ then \underline{P}⟶^{α}_{t}\underline{P}′ for some \underline{P}′ with (\underline{P}′, \underline{Q}′) ∈ R.

Two agents \underline{P} and \underline{Q} are bisimilar, denoted by \underline{P} ∼_{T} \underline{Q}, if there is a strong temporal bisimulation R with (\underline{P}, \underline{Q}) ∈ R.

Remark Since ℓTCCS is a sublanguage of Timed CCS, it is easily to see that ∼_{T} coincides with strong equivalence ∼ of Chapter 5. Therefore ∼_{T}, the largest temporal bisimulation, is an equivalence relation and also a congruence relation, i.e. it is fully substitutive. □

We now consider an interpretation of CCS over ℓTCCS. Our interpretation is based on a postulation that between any two actions which are causally related, there is some non-zero delay Δ. We can understand the postulation as that every atomic action has a duration Δ. The interpretation is then defined by the following.

Definition 8.2.3

\begin{matrix}T (nil) = \underline{nil} & T (P + Q) = T (P) + T (Q) \\ T (α.P) = \underline{α}.(Δ).T (P) & T (P | Q) = T (P) | T (Q) \end{matrix}

We now define a timed equivalence on CCS.

Definition 8.2.4 For any CCS processes P and Q, we say P and Q are timed equivalent, written as P ∼_{T} Q, if T (P) ∼_{T} T (Q).

Timed equivalence ∼_{T} over CCS distinguishes more things than strong equivalence. For example,

a | b ≁_{T} a | b + ab

Moreover, timed equivalence ∼_{T} over CCS has more discriminating power than pomset bisimulation of [BC87]. As an example, we have

a | b + a(b + c) + ab ≁_{T} a | b + a(b + c)

We actually believe that our timed equivalence over CCS is the same as the partial order bisimulation of [DDM89] as described in Section 8.1.

8.3 Conclusion

In the usual operational semantics of CCS and the related observational equivalence, atomic actions are instantaneous indivisible events. However it can be argued that every atomic action will take some time. In this chapter, we postulated that every atomic action has a non-zero constant duration. We satisfied this by assuming that for any two atomic actions which are causally related there is at least a non-zero constant delay Δ between them. Based on this postulation, we translated CCS processes into timed processes of ℓTCCS and thus gave a timed equivalence for CCS (the induced equivalence). The resulting equivalence has more discriminating power than strong equivalence and distinguishes concurrency from nondeterminism. It is in fact a partial order or true concurrency semantics.

The importance of the timed semantics for CCS is in the use of an interleaving model for partial order or true concurrency semantics. This suggests an interleaving approach for the study of true concurrency semantics. It is well known that the interleaving approach is simple and has elegant mathematical techniques. In Chapter 6, we presented a simple proof system for deciding timed equivalence. With the result of this chapter, it can also be used for partial order or true concurrency.

In [Hen88b], Hennessy also postulated that every external action (non-τ action) has a duration. Rather than associate specific durations with actions, he introduced observers which could distinguish the inception of an action from its termination. The observational equivalence based on those new observers also distinguished concurrency from nondeterminism. However, since the internal action τ was still instantaneous, one could not differentiate the process a|τ from the process a|τ + τa in the strong version of Hennessy’s equivalence.

Conclusions and Future Work

In this thesis, we presented a timed calculus, Timed CCS, which is a general model of concurrency. We made no assumptions about the underlying nature of time, allowing it to be discrete or dense. Timed CCS can be used for the specification and verification of real-time systems. We gave some examples to show the uses of the calculus for formalising three important notions, time out, duration control and time dependency, of real-time systems. We studied the theory of the abstract semantics of Timed CCS and provided a mathematical model for a wide range of timed calculi including Timed CCS. Timed CCS is an interleaving model for real-time systems. If we postulate that every atomic action has a non-zero constant duration, then we can observe the usual notions of causality, concurrency and conflict relations between events of a system. We satisfied the postulation by insisting that for any two causally related events there is at least a non-zero constant delay between them. By interpreting CCS in a sublanguage ℓTCCS of Timed CCS and TCCS [MT90] based on this postulation, we developed a partial order or true concurrency semantics for CCS. As a consequence, we have developed a partial order semantics by using an interleaving approach.

There are a few problems which are worth future work. In Chapter 5, we presented a simple modal logic which is an extension of Hennessy-Milner logic with time. We showed the modal characterization of strong bisimulation. This in turn suggested that modal logic is an appropriate logic for the specification and verification of non-deterministic, concurrent and real-time systems. In order to support modular design and verification of systems in this framework, the problem of compositionality of modal assertions arose. This problem has been successfully dealt with by Stirling [Sti87] and Winskel [Win84b] for CCS and SCCS. Also a formula of our modal logic is only capable of describing those properties which only concern certain finite behaviours of processes. As a consequence, it is impossible to use a formula to describe properties of processes which are to hold invariantly or eventually. All these properties are clearly important in practice. By extending the modal logic with infinite connectives, these invariant and eventual properties are expressible. However we are also concerned with the problem of verifying when a process satisfies a formula. This requires us to insist that all formulas of our logic should be finitary expressions. In [Lar88], Larsen presents proof systems for Hennessy-Milner logic with recursion. As future work, we can consider how to incorporate time into modal μ-calculus and study compositional proof systems for Timed CCS.

In Chapter 8, we studied the theory of behavioural abstraction in timed processes. As the timed version of Hennessy’s theorem, which says that P ≈ Q implies P =^{+} Q or τ.P =^{+} Q or P =^{+} τ.Q, no longer holds, this leaves the completeness problem of observational congruence of timed processes hard and still open. However, if we restrict ourselves to a special case and assume maximal progress, then we can retain Hennessy’s theorem for timed processes and the solution to the problem is straightforward.

In [MT91], Moller and Tofts have proposed a faster than preorder on concurrent processes which distinguishes between functionally behaviourally equivalent processes operating at different speeds. For timed processes, timing also implicitly introduces a causality relation between events. For example, in process a(t)_{0}^{5}. nil | b(s)_{10}^{15}. nil, action b can only occur after the occurrence of action a. Since we do not distinguish between the causality introduced explicitly by the prefix operator and the causality introduced implicitly by timing, this leads to the faster than preorder being a precongruence only when we do not allow the notion of time out (e.g. for Timed CCS, the upper bound e′ of prefix α(t)_{e}^{e′}. E must be the infinite time ∞). It would be nice if we could have some preorder which is also a precongruence for a language allowing time out notion, e.g. Timed CCS or TCCS of [MT90].

Another interesting topic is adding probabilities to Timed CCS. This may enable us to consider temporal, probabilistic and computational behaviour simultaneously. The resulting calculus would be expressively powerful to represent notions of safety, liveness and fairness. This would facilitate the unification and comparison of different models of concurrency and promote a deep understanding of concurrency.

Bibliography

[AD90] R. Alur & D. Dill, Automata for Modelling Real-Time Systems Proc. IC-ALP’90, Lecture Notes in Computer Science 443, pp 322-335, 1990

[ACD90] Model-Checking for Real-Time Systems, Proc. of LICS’90, pp 414-425, 1990

[ACM92] S. Anderson, L. Chen & F. Moller, Observing Causality in Real-Timed Calculi, Draft Note, LFCS, University of Edinburgh, 1992

[BB91] J.C.M. Baeten & J.A. Bergstra, Real Time Process Algebra, Formal Aspects of Computing, Vol 3, No 2, pp142-188, 1991

[BKR86] M. Ben-Or, D. Kozen & J. Reif, The Complexity of Elementary Algebra and Geometry, Journal of Computer and System Sciences, 32, pp 251-264, 1986

[BK84] J.A. Bergstra & J.W. Klop, Process Algebra for Synchronous Communication, Information and Control 60(1-3), pp. 109-137, 1984

[BK85] J.A. Bergstra & J.W. Klop, Algebra of Communicating Processes with Abstraction, Theoretical Computer Science 37, pp 77-12, 1985

[BC87] G. Boudol & I. Castellani, On the Semantics of Concurrency: Partial Order and Transition Systems, Proc. of TAPSOFT-CAAP’87, Lecture Note in Computer Science 249, pp 123-137, 1987 [BC89] G. Boudol & I. Castellani, Permutation of Transitions: An Event Struc-

ture Semantics for CCS and SCCS, Proc. of Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, Lecture Notes in Computer Science 354, pp 411-427, 1989

[BS92] J. Bradfield & C. Stirling, Local Model Checking for Infinite State Spaces, Theoretical Computer Science 96, pp 157-174, 1992

[BHR84] S.D. Brookes, C.A.R. Hoare & A.D. Roscoe, A Theory of Communicating Sequential Processes, Journal of the ACM, Vol. 31, No. 3, 1984

[Cer92] K. Cerans, Decidability of Bisimulation Equivalences for Parallel Timer Processes, in Proc. of the 4th Workshop on Computer-Aided Verification, 1992

[Cle90] R. Cleaveland, Tableau-based Model Checking in Propositional mu-Calculus, Acta Inform. 27, pp 725-747, 1990

[Che91a] L. Chen, Specification and Verification of Real-Time Systems, Draft Note, LFCS, University of Edinburgh, 1991

[Che91b] L. Chen, Decidability and Completeness in Real-Time Processes, Technical Report ECS-LFCS-91-185, Edinburgh University, 1991

[Che92] L. Chen, An Interleaving Model for Real-Time Systems, in Proc. of Symp. of Logical Foundations of Computer Science, Lecture Notes in Computer Science 620, pp 81-92, 1992

[Che93] L. Chen, Axiomatising Real-Time Processes, will appear in Proc. of MFPS IX, Lecture Notes in Computer Science, April, 1993

[CAM90] L. Chen, S. Anderson & F. Moller, A Timed Calculus of Communicating System, Technical Report ECS-LFCS-90-127, University of Edinburgh, 1990 [CM92] L. Chen & A. Munro, Applications of Modal Logic for the Specifications

of Real-Time Systems, will appear in Proc. of FME’93, Lecture Notes in Computer Science, April, 1993

[Col75] G. E. Collins, Quantifer Elimination for Real Closed Fields by Cylindric Algebraic Decomposition, Proc. 2nd GI Conference on Automata Theory and Formal Language, pp 134-183, 1975

[DS89] J. Davies & S. Schneider, An Introduction to Timed CSP, PRG-75, Programming Researcg Group, Oxford University, 1989

[DDM89] P. Degano, R. De Nicola & U. Montanari, Partial Orderings Descriptions and Observations of Nondeterministics Concurrent Processes, Proc. of Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, Lecture Notes in Computer Science 354, pp 438-466, 1989

[End72] H. B. Enderton, A Mathematical Introduction to Logic, Academic Press, Inc., 1972

[Gro90] J.F. Groote, Specification and Verification of Real Time Systems in ACP, Proc. of 10th International symp. on Protocol Specification, Testing and Verrification, Ottawa, 1990

[Hen85] M. Hennessy, Acceptance Trees, Journal of the Association for Computing Machinery, Vol 32, No 4, pp 896-928, 1985

[Hen88a] M. Hennessy, Algebraic Theory of Processes, The MIT Press, 1988

[Hen88b] M. Hennessy, Axiomatising Finite Concurrent Processes, SIAM J. Comput. Vol 17, No 5, pp 997-1017, 1988

[Hen91] M. Hennessy, A Proof System for Communicating Processes with Value-Passing, Formal Aspects of Computing, Vol3, No 4, pp 346-366, 1991 [HM85] M. Hennessy & R. Milner, Algebraic Laws for Nondeterministic and Con-

currency, J. Assoc. Comput. Mach. 32, pp 137-161, 1985

[HR90] M. Hennessy & T. Regan, A Temporal Process Algebra, Technical Report 2/90 University of Sussex, 1990

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

[HLW91] U. Holmer, K. Larsen & Y. Wang, Deciding Properties of Regular Real Time Processes, in CAV’91, Lecture Notes in Computer Science, 1991.

[Kel76] R. Keller, Formal Verification of Parallel Programs, Communication of the ACM, Vol. 19, No. 7, 1976

[Klu91] A.S. Klusener, Completeness in Real Time Process Algebra, Proceedings of CONCUR’91, Lecture Notes in Computer Science 527, pp 96-110, 1991

[Lar88] K. Larsen, Proof systems for Hennessy-Milner Logic with Recursion, Lecture Notes in Computer Science 299, 1988

[LL90] K. Larsen & X. Liu, Compositionality through an Operational Semantics of Contexts, Proc. ICALP’90, Lecture Notes in Computer Scuence 443, pp 526-539, 1990

[Mil80] R. Milner, A Calculus of Communicating systems, Lecture Notes in Computer Science 92, Springer-Verlag, 1980

[Mil83] R. Milner, Calculi for Synchrony and Asynchrony, Theoretical Computer Science, 25, pp 267-310, 1983

[Mil89a] R. Milner, Communication and Concurrency, Prentice-Hall International, 1989 [Mil89b] R. Milner, A Complete Axiomatisation for Observational Congruence of

finite-state Behaviours, Information and Computation 81, pp. 227-247, 1989

[Mol89] F. Moller Axioms for Concurrency, Ph.D Thesis, CST-59-89, University of Edinburgh, 1989

[Mol90] F. Moller, Process Algebra as a Tool for Time Analysis, in IV Banff Higher Order Workshop, Springer-Verlag Workshops in Computer Science, 1990

[MT90] F. Moller & C. Tofts, A Temporal Calculus of Communicating System, Proc. of CONCUR’90, Lecture Notes in Computer Science 458, pp 401-415, 1990

[MT91] F. Moller & C. Tofts, Relating Processes With Respect to Speed, Proc. of CONCUR’91, Lecture Notes in Computer Science 527, 1991

[Sif90] X. Nicollin, J. Richier, J. Sifakis & J. Voiron, ATP : an Algebra for Timed Processes, Laboratoire de Genie Informatique, IMAG-Campus, 38041 Grenoble Cedex, France, 1990

[NPW81] M. Nielsen, G. Plotkin & G. Winskel, Petri Nets, Event Structures and Domains, Theoretical Computer Science 13, pp 85-108, 1981

[Par81] D.M.R. Park, Concurrency and Automata on Infinite Sequences, Proc. of ICALP’81, Lecture Notes in Computer Science 104, Springer-Verlag, 1981

[Plo81] G.D. Plotkin, A Structured Approach to Operational Semantics, DAIMI FN-19, Computer Science Department, Arhus University, Denmark, 1981

[RR88] R. Reed & A. W. Roscoe, A Timed Model for Communicating Sequential Processes, Theoretical Computer Science, 58, pp 249-261, 1988

[Rei85] W. Reisig, Petri Nets: an Introduction, EATCS Monographs, Springer-Verlag, 1985 [SM92] D. Sangiogi & R. Milner, The Problem of “Weak Bisimulation Up To”,

LFCS, University of Edinburgh (submitted for publication), 1992

[Sch91] S. Schneider, An Operational Semantics for Timed CSP, in Proc. of Chalmers Workshop on Concurrency, 1991.

[Smy78] M. B. Smyth, Power Domains, Journal of Computer and Systems Science 16, 1978

[Sti87] C. Stirling, Modal Logics for Communication Systems, Theoretical Computer Science 49, pp. 311-347, 1987

[Sti91] C. Stirling, Modal and Temporal Logics in Handbook of Logic in Computer Science, edited by S. Abramsky, D. Gabbay & T. Maibaum (also as Technical Report ECS-LFCS-91-157, University of Edinburgh), 1991

[SW89] C. Stirling & D. Walker, Local Model Checking in the Propositional μ-Calculus, Proc. of TAPSOFT’89, Lecture Notes in Computer Science 351, pp 369-383, 1989

[Tof91] C. Tofts, Proof Methods and Pragmatics for Parallel Programming, Ph.D Thesis, CST-74-91,University of Edinburgh, 1991

[Wan90] Y. Wang, Real-time Behaviour of Asynchronous Agents, Proc. of CON-CUR’90, Lecture Notes in Computer Science 458, pp 502-520, 1990

[Wan91] Y. Wang, CCS + Time = an Interleaving Model for Real Time Systems, Proc. of ICALP’91, Lecture Notes in Computer Science 1991

[Win83] G. Winskel, Event Structure Semantics for CCS and Related Languages, Lecture Notes in Computer Science 140, pp 561-576, 1983

[Win84a] G. Winskel, Synchronization Trees, Theoretical Computer Science 34, pp32-82, 1984 [Win84b] G. Winskel, On the Composition and Decomposition of Assertions, Proc.

of Seminar on Concurrency, Lecture Notes in Computer Science 197, 1984

[Win87] G. Winskel, Event Structures, Proc. of Petri Nets: Applications and Relations to Other Models of Concurrency, Lecture Notes in Computer Science 255, pp 325-392, 1987

[Win89] G. Winskel, Model Checking the Modal ν-Calculus, in Proc. ICALP’89, Lecture Notes in Computer Science, 1989