An Interleaving Model for Real-Time Systems

Liang Chen^{1}

Laboratory for the Foundations of Computer Science Department of Computer Science University of Edinburgh Edinburgh EH9 3JZ, UK

September 15, 1991

Abstract

In this paper, we present a general interleaving model for real-time systems which is an extension of Milner’s CCS with time. We make no assumption about the underlying nature of time, allowing time to be discrete (such as the integers) or dense (such as the rationals or the reals). We also make no assumption of the Maximal Progress Principle. The time variables allow us to represent the notion of time dependency and thus the language is more expressive than those without time variables. We extend bisimulations to timed processes and study the theories of strong equivalence, weak equivalence and observational congruence. Also we show that strong equivalence is decidable for finite processes, i.e. the processes without recursion. The decidability is independent of the choice of time domain.

1 Introduction

Process algebras, such as CCS [Mil80, Mil89], CSP [Hoa85] and ACP [BK84, BK85], are structured description languages for concurrent systems and have a variety of well developed semantic theories and verification methods. They are considered to be very successful specification languages. However, none of them consider the time aspects of concurrent systems. Instead they usually deal with the quantitative aspects of time of a concurrent system in a qualitative way and ignore explicit time information. There are many systems and applications, such as real-time systems in which interactions with the environment must satisfy some time constraints, for which purely qualitative specification and analysis are inadequate.

1The author is supported by TC Scholarship. e-mail: cl@dcs.ed.ac.uk

Recently there have been a number of attempts to introduce time in process algebras. The works include extensions of Milner’s CCS with time [CAM90, HR90, MT90, Wan90], extensions of Hoare’s CSP with time [RR88] and extensions of Bergstra and Klop’s ACP with time [BB91, Gro90, Sif90]. Among these works, there are many features in common. Works such as [HR90, Gro90, Sif90] only deal with discrete time and introduce a special action to represent one unit of time. In general, these languages cannot express the notion of time dependency. For example, consider a system M which can perform action a followed by action b. Action a may happen at any time t. If a happens at time t, then action b must happen before a further t time. Clearly, we cannot define the system M in these languages. Some works, such as [CAM90, Wan90, RR88, HR90], are based on an assumption of the Maximal Progress Principle and therefore are not general.

In this paper, we explore the possibility of incorporating time in a well developed process algebra. We present a more general interleaving model for realtime systems. The work is based on Milner’s CCS. We make no assumption about the underlying nature of time, allowing time to be discrete (such as the integers) or dense (such as the rationals or the reals). The time variables allow us to represent the notion of time dependency in the language. Also we make no assumption of the Maximal Progress Principle, but the whole theory is consistent with the principle.

The 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. We say two actions happen at the same time if one action follows the other instantaneously. To be more realistic, we may insist that for any two actions which are causally related, there should be some non-zero constant delay between them.

In section 2, we present the formal syntax and semantics of the language. In section 3, we define some derived operators and give some examples to demonstrate the utility of the language serving for the specification of real-time systems. In section 4, we define strong bisimulation over timed processes and study the properties of strong equivalence. We show that weakly guarded equations have an unique solution up to strong equivalence. Also, we show that the strong equivalence is decidable for finite processes, i.e. those processes without recursion. The decidability is independent of the choice of time domain. In section 5, we discuss behaviour abstraction for timed processes. We define weak bisimulation and C-bisimulation for timed processes and study the properties of weak equivalence and observation congruence. We show that sequential and guarded equations have an unique solution up to observational congruence.

2 Syntax and Semantics

2.1 The Language of Timed CCS

To define Timed CCS, we presuppose a set Λ, 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. a and ā are called complementary actions which form the basis of communications in our language, analogous to CCS. We also presuppose an infinite set Tvar of time variables, ranged over by t, s, r. Let the time domain be (T ⋃{∞}, ≤), where T contains an 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 to be N (the set of the integers), Q (the set of the rationals) or R (the set of the reals). We introduce ∞ to represent infinite time. Time expressions, ranged over by e, f, g, are defined as follows:

Definition 2.1

1 For any u ∈ T and t ∈ Tvar, u and t are time expressions.

2 If e and f are time expressions, then e+f, 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 also presuppose an infinite set Pvar 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 expressions, where S : Λ ⟶ Λ is a relabelling function which satisfies \overline{S(a)} = S(ā). Also, by convention, S(τ) = τ.

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

where e′ is a time expression or e′ ≡ ∞ (≡ is the syntactical equality).

The informal interpretation of the language is as follows:

1. X represents the process bound to it.

2. nil represents the process which does no action, but idles any time.

3. α(t)_{e}^{e′}. E represents the process which performs action α between time e and e′, after α happens, it evolves to process E{u/t}, where u is the time at which α happens and E{u/t} is the result of substituting all free occurrences of t in E.

4. E + F represents deterministic and nondeterministic choice between processes E and F. The choice is made at the time of the first action of E or F, or at times when one process can idle but another cannot. So the choice is deterministic with time proceeding.

5. E|F represents the parallel composition of processes E and F. Each of them may perform actions independently, or they synchronise on complementary actions which represent communications between them. Parallel composition must be synchronous with time proceeding.

6. E\a represents the process which behaves as E, but action a and its complementary action ā are forbidden.

7. E[S] represents the process resulting from E by relabelling its actions using S.

8. μX.E represents the process defined by equation X = E.

There are two kinds of variables: time variables and process variables. The operator α(t)_{e}^{e′}. in α(t)_{e}^{e′}. E binds all free occurrences of time variable t in E. The 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 time variables (process variables). We use ftv(E) (fpv(E)) to represent the set of all free time (process) variables occurring in E. We identify those process expressions which are the same up to change of bound time and process variables. A process expression E is closed with respect to time variables (process variables) if there is no free occurrences of time variables (process variables) in 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, ranged over by P, Q, R.

2.2 The Operational Semantics of Timed CCS

In order to define a semantics for Timed CCS, we use the labelled transition system

(P, {⟶^{α}_{u} ⋃ ⟶_{u} | α ∈ Act ⋀ u ∈ T })

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 need to formalise a notion of maximum delay times of processes before any actions.

Definition 2.2 For any process E, its maximum delay time |E|_{T} is defined inductively as follows |X|_{T} = 0 |nil|_{T} = ∞ |α(t)_{e}^{e′}. E|_{T} = max(0, e′) |E + F |_{T} = max(|E|_{T} , |F |_{T}) |E | F |_{T} = min(|E|_{T} , |F |_{T}) |E\a|_{T} = |E|_{T} |E[S]|_{T} = |E|_{T} |μX.E|_{T} = |E|_{T}

For example, |μX.α(t)_{1}^{8}. X + X|_{T} = 8 and |μX.α(t)_{1}^{8}. X | X|_{T} = 0

Table 1 presents transition rules of the language. 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 1. Notation δ =^{def} (a(t)_{0}^{0}. nil)\a

Informally, δ represents a dead process which neither performs any action, nor idles. Proposition 2.1 (1) For any agent P, P ⟶_{0}P.

(2) For any agent P and u ∈ T , P ⟶_{u}P′ for some P′ if and only if u ≤ |P |_{T}. By induction on P, the result follows from the definition of transition rules.

3 Derived Operators and Examples

3.1 Derived Operators

We may define some useful operators in the language. The first one is time prefix (e)E for any time expression e and weakly guarded process E. We say a process E is weakly guarded if every occurrence of process variables is guarded by some action. For example, if X is weakly guarded in E, then X can only occur in some subterm of form α(t)_{e}^{e′}. F. Definition 3.1 For any time expression e and weakly guarded process E, we define (e)E inductively on E as follows:

\overline{P ⟶_{0}P}

\overline{α(t)_{e}^{e′}. P ⟶^{α}_{u}P \{u/t\}} max(0, e) ≤ u ≤ e′

\overline{α(t)_{e}^{e′}. P ⟶_{u}α(t)_{e ˙−u}^{e′−u}. (P \{u + t/t\})} 0 ≤ u ≤ e′

\overline{nil⟶_{u}nil}  u ≥ 0  \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 1: Operational Semantics (e)nil = nil

(e)(a(t)_{f}^{f′}. E) = a(t)_{f+e}^{f′+e}. (E{t − e/t}) 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, (e)P represents a process which will idle time e and then behave as process P.

Note that ∞ is not a time expression, for convenience, we use (∞)δ in place of (a(t)_{0}^{∞}. nil)\a in the sequel.

We can also define the time shift e >> E of [BB91], where e is a time expression and E is a weakly guarded process.

Definition 3.2 For any time expression e and weakly guarded process E, the time shift e >> E is defined inductively over E as follows:

e >> nil = nil

e >> (a(t)_{f}^{f′}. E) = a(t)_{f ˙−e}^{f′−e}. (P {t + e/t}) 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 P, e >> P represents the result of P after idling time e without any action. So we have following property:

Proposition 3.1 For any agent P, P ⟶_{u}u >> P, where 0 ≤ u ≤ |P |_{T}.

In Timed CCS, we represent explicitly the notion of timeout. For example, in a(t)_{2}^{10}. nil + (15)δ, the timeout of action a is 10 seconds (if we measure time in seconds) and after 10 seconds action a is blocked. Also, we can define another important notion, duration control, of real-time systems in Timed CCS. Consider a process E which may behave as process E′ before time e and from time e it must behave as process E′′. We use E′ U_{e}E′′ to represent such a process. To simplify the definition of E′ U_{e}E′′, we assume that for every relabelling function S, there is a relabelling function S^{−1}, the inverse function of S, such that SS^{−1} = S^{−1}S = id, where id is the identity function.

Definition 3.3 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/λ] λ is a fresh action for E, F.

(E[S]) U_{e}F = (E U_{e}(F [S^{−1}]))[S]

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

3.2 Examples

In this section, we give some examples to show the utility of the language serving for the specification of real-time systems.

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

Sender, after accepting a message from the environment, sends it with an attached bit b, where b = 0 or 1, along the line Trans. Then it waits for an appropriate acknowledgement within time D, the time Sender will wait after sending a message before assuming the message had been lost and retransmitting it. 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 bit b̂. If it get a wrong acknowledgement or does not receive any acknowledgement within time D, Sender retransmits the message at time D + Δ. Sender = Sender_{0} Sender_{b} = accept(t)_{0}^{∞}. (Δ) \overline{send}_{b}(s)_{0}^{0}. (Δ) Sending_{b}

Sending_{b} = ackb̂(t)_{0}^{D}. (Δ) \overline{send}_{b}(s)_{0}^{0}. (Δ) Sending_{b} +

ack_{b}(t)_{0}^{D}. (Δ) Senderb̂ + (D + Δ) \overline{send}_{b}(s)_{0}^{0}. (Δ) Sending_{b}

Receiver, which we assume starts in a state waiting for a message tagged with 0, is defined as: Receiver = tran_{0}(t)_{0}^{∞}. (Δ) Deliver_{0} Deliver_{b} = \overline{deliver}(t)_{0}^{0}. (Δ) \overline{reply}_{b}(s)_{0}^{0}. (Δ) Reply_{b}

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

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

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

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

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

Ack = reply_{0}(t)_{0}^{∞}. (Δ) (τ(s)_{0}^{D′}. (Δ) Ack + (D′) \overline{ack}_{0}(s)_{0}^{0}. (Δ) Ack)

+ reply_{1}(t)_{0}^{∞}. (Δ) (τ(s)_{0}^{D′}. (Δ) Ack + (D′) \overline{ack}_{1}(s)_{0}^{0}. (Δ) Ack)

Now we may define the protocol as

P rotocal = (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 transition lines, we should take the timeout D > 2D′ + 4Δ.

Example 2 (Duration Control) Consider a login procedure. After a terminal is connected to the 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 pass the control to a process Q which formalizes the user’s task. If the user’s login response is invalid, the system goes back and still waits for user’s valid response. After waiting for 2 minutes without any valid response, the system rejects the current login request and the connection between the terminal and the system is broken.

LP = connect(t)_{0}^{∞}. (Δ) (P | (b(t)_{0}^{∞}. Q + a(t)_{0}^{∞}. nil)\{a, b}

P = L U_{2} ā(s)_{0}^{0}. LP

L = r(t)_{0}^{∞}. (Δ) b̄(t)_{0}^{0}. nil+ir(t)_{0}^{∞}. (Δ)L

4 Strong Equivalence and its Properties

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.

Definition 4.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 there is some Q′ such that Q⟶^{α}_{u}Q′ and (P′, Q′) ∈ R.

(2) if P ⟶_{u}P′, then there is some Q′ such that Q⟶_{u}Q′ and (P′, Q′) ∈ R.

(3) if Q⟶^{α}_{u}Q′, then there is some P′ such that P ⟶^{α}_{u}P′ and (P′, Q′) ∈ R.

(4) if Q⟶_{u}Q′, then there is some P′ such that P ⟶_{u}P′ and (P′, Q′) ∈ R.

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.2 ∼ = ⋃ {R | R is a strong bisimulation}.

Proposition 4.1 ∼ is the largest strong bisimulation. Moreover, ∼ is an equivalence relation.

The proof follows from the facts that the union, composition and converse of strong bisimulations are still strong bisimulations and also the identity over agents is a strong bisimulation.

Lemma 4.2 For any agents P and Q, P ∼ Q implies |P |_{T} = |Q|_{T}.

Definition 4.3 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 there is a Q′ such that Q⟶^{a}_{u}Q′ and (P′, Q′) ∈ R.

(2) if Q⟶^{a}_{u}Q′, then there is a P′ such that P ⟶^{a}_{u}P′ and (P′, Q′) ∈ R.

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

Similar to that of 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.4 ∼_{T} = ⋃ {R | R is a strong T −bisimulation}

Proposition 4.3 ∼_{T} is the largest strong T -bisimulation. Moreover, ∼_{T} is an equivalence relation.

Lemma 4.4 (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′′

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

The proof follows from the definition of transition rules. (1) shows the property of time determinacy. (2) and (3) show the property of time continuity and (4) says that atomic actions are instantaneous.

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

Proof (⇒) It is easy to show that ∼ is a strong T -bisimulation. (⇐) We prove P ≁ Q implies P ≁_{T} Q by induction on the maximum depth of P and Q, where the depth of P is defined to be the maximum number of nested actions in P. Suppose P ≁ Q, then it must be one of the following cases:

Case 1 P ⟶^{α}_{u}P′ and for any Q′, if Q⟶^{α}_{u}Q′ then P′ ≁ Q′. By induction, if

Q⟶^{α}_{u}Q′ then P′ ≁_{T} Q′. So P ≁_{T} Q.

Case 2 Q⟶^{α}_{u}Q′ and for any P′, if P ⟶^{α}_{u}P′ then P′ ≁ Q′. Similar to case (1).

Case 3 |P |_{T} ≠ |Q|_{T}, clearly, P ≁_{T} Q.

Case 4 All above cases do not hold for P and Q, this is impossible. Otherwise, let R = {(P′, Q′) | (P′ = P ⋀ Q′ = Q) ⋁ ∃u ≤ |P |_{T} .(P ⟶_{u}P′ ⋀ Q⟶_{u}Q′)} ⋃ ∼. It is easy to show that R is a strong bisimulation. So P ∼ Q, contradiction. □

The reason that strong bisimulation and strong T -bisimulation coincide is because time is deterministic, i.e. the transition ⟶_{u} is deterministic. Since the maximal idle time of an agent is syntacticly defined, it will be easier to show a relation of strong T -bisimulation than that of strong bisimulation.

4.2 Some Properties of Strong Equivalence

In this section, we show some equational laws for strong equivalence. By using these laws (note that every law can be regarded as two direction rewriting rule), every process can be rewritten into a special form which we call the normal form.

Proposition 4.6 (Laws for Prefix)

1 a(t)_{e}^{e′}. P ∼ a(s)_{e}^{e′}. (P {s/t}) s is free for t in P

2 a(t)_{e}^{e′}. P ∼ (max(0, e′))δ e > e′

3 a(t)_{e}^{e′}. P ∼ a(t)_{e}^{e′}. P + (max(0, e′))δ

4 a(t)_{e}^{f}. P + a(t)_{f}^{e′}. P ∼ a(t)_{e}^{e′}. P e ≤ f ≤ e′ All these laws may be proved by showing appropriate strong bisimulations.

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

Similarly, all these laws may be proved by exhibiting appropriate strong T - bisimulations. These laws together say that (P, +, δ) is a monoid. Proposition 4.8 (Laws for Restriction) 1 (∞)δ ∼ nil 2 nil\a ∼ nil 3 (α(t)_{e}^{e′}. P)\a ∼ α(t)_{e}^{e′}. (P \a) α ≠ a ⋀ α ≠ ā 4 (α(t)_{e}^{e′}. P)\a ∼ (max(0, e′))δ α = a ⋁ α = ā 5 (P + Q)\a ∼ P \a + Q\a

Since the restriction operator is distributive over choice, for any agent P which does not contain the parallel operator, we can get an agent P′ by using these laws (regarding every law as a two direction rewriting rule) such that P ∼ P′, where P′ does not contain the restriction operator (except δ). Proposition 4.9 (Laws for Relabelling) 1 ((e)δ)[S] ∼ (e)δ 2 (α(t)_{e}^{e′}. P)[S] ∼ (S(α))(t)_{e}^{e′}. (P [S]) 3 (P + Q)[S] ∼ P [S] + Q[S]

Similarly, for any agent P which does not contain the parallel operator, we can find an agent P′ by using these laws such that P ∼ P′ , where P′ does not contain the relabelling operator. Proposition 4.10 (Laws for Recursion)

1 P ∼ E if P =^{def} E.

2 μX.E ∼ E{μX.E/X}

Up to now, we have only defined strong equivalence over agents. However, we may also extend strong equivalence to any processes in the standard way.

Definition 4.5 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 4.6 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⃗}.

Clearly, all laws discussed before still hold for processes. Moreover, we have the following expansion law. To simplify the presentation, we need a notion of normal form.

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

Proposition 4.11 (Expansion Law) Given

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)δ

in normal forms, then

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 some fresh time variables.

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

(1) ∼_{T} ⊆ R.

(2) For any normal forms P ≡ ∑_{i∈I} α_{i}(t_{i})_{e_{i}}^{e′_{i}}. P_{i} +(u)δ and Q ≡ ∑_{j∈J} β_{j}(s_{j})_{f_{j}}^{f′_{j}}. Q_{j} + (v)δ, let G be the right hand side of expansion law for P and Q, then (P | Q, G) ∈ R

is a strong T -bisimulation. 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}, max(0, e_{i}) ≤ u ≤ e′_{i}, P′ ≡ P_{i}{u/t_{i}} and Q′ ≡ u >> Q.

Clearly, G⟶^{α}_{u}(P_{i}{r_{i}/t_{i}} | r_{i} >> Q){u/r_{i}} ∼_{T} R.

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} = ā, max(0, e_{i}, f_{j}) ≤ u ≤ min(e′_{i}, f′_{j}), P′ ≡ P_{i}{u/t_{i}} and Q′ ≡

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

∼_{T} R. Case 2 Suppose G⟶^{α}_{u}R. Similar to case 1. Case 3 |P | Q|_{T} = min(u, v) = |G|_{T}. □

Strong equivalence is a congruence relation, asshown by the following two propositions. Proposition 4.12 For any processes E and F, E ∼ F implies 1 α(t)_{e}^{e′}. E ∼ α(t)_{e}^{e′}. F 2 E + G ∼ F + G 3 E | G ∼ F | G 4 E\a ∼ F \a 5 E[S] ∼ F [S]

All of these properties can be shown by exhibiting appropriate strong bisimulations. In the sequel, E⃗ ∼ F⃗ represents componentwise strong equivalences between E⃗ and F⃗. Proposition 4.13 For any processes E⃗ and F⃗ which contain at most free process variables X⃗, E⃗ ∼ F⃗ implies μX⃗.E⃗ ∼ μX⃗.F⃗.

Proof We only deal with a single recursive equation. Let E and F be closed with respect to time variables and contain at most free process variable X. Suppose E ∼ F. To show μX.E ∼ μX.F, it is enough to show (by taking G ≡ X) that

{(G{μX.E/X}, G{μX.F/X}) | fpv(G) ⊆ {X} and ftv(G) = ∅}

is a strong bisimulation up to ∼. To do that, it is enough to prove (by the symmetric arguments) that

1 If G{μX.E/X}⟶_{u}P′, then for some Q′ and Q′′, G{μX.F/X}⟶_{u}Q′′ with Q′′ ∼ Q′ and (P′, Q′) ∈ S.

2 If G{μX.E/X}⟶^{α}_{u}P′, then for some Q′ and Q′′, G{μX.F/X}⟶^{α}_{u}Q′′ with

Q′′ ∼ Q′ and (P′, Q′) ∈ S.

We prove the claim by transition induction on the depth of inferences.

1. Suppose G{μX.E/X}⟶_{u}P′. Consider the cases for G.

Case 1 G ≡ X.

Then μX.E⟶_{u}P′ and thus E{μX.E/X}⟶_{u}P′. By induction, for some Q′ and Q′′, E{μX.F/X}⟶_{u}Q′′ with Q′ ∼ Q′′ and (P′, Q′) ∈ S. Since E ∼ F, we have F {μX.F/X}⟶_{u}Q′′′ and Q′′ ∼ Q′′′. Thus μX.F ⟶_{u}Q′′′ with Q′ ∼ Q′′′ and (P′, Q′) ∈ S.

Case 2 G ≡ α(t)_{v}^{v′}. G′.

Then

G{μX.E/X} ≡ α(t)_{v}^{v′}. (G′{μX.E/X})

and

P′ ≡ α(t)_{v ˙−u}^{v′−u}. (G′{μX.E/X}){t + u/t}

where 0 ≤ u ≤ v′, Also

G{μX.F/X} ≡ α(t)_{v}^{v′}. (G′{μX.F/X})⟶_{u}α(t)_{v ˙−u}^{v′−u}. (G′{μX.F/X}){t+u/t}

Since μX.E and μX.F are closed with respect to time variables, we have

α(t)_{v ˙−u}^{v′−u}. (G′{μX.E/X}){t + u/t} ≡ (α(t)_{v ˙−u}^{v′−u}. G′{t + u/t}){μX.E/X}

and

α(t)_{v ˙−u}^{v′−u}. (G′{μX.F/X}){t + u/t} ≡ (α(t)_{v ˙−u}^{v′−u}. G′{t + u/t}){μX.F/X}

Case 3 G ≡ G_{1} | G_{2}.

Then G_{1}{μX.E/X}⟶_{u}P_{1}, G_{2}{μX.E/X}⟶_{u}P_{2} and P′ ≡ P_{1} | P_{2}. By induction

G_{1}{μX.F/X}⟶_{u}Q′_{1} with Q′_{1} ∼ Q_{1} and (P_{1}, Q_{1}) ∈ S

and

G_{2}{μX.F/X}⟶_{u}Q′_{2} with Q′_{2} ∼ Q_{2} and (P_{2}, Q_{2}) ∈ S

Let Q′ ≡ Q_{1} | Q_{2}, then G{μX.F/X}⟶_{u}(Q′_{1} | Q′_{2}) ∼ Q′. It remains to show that (P′, Q′) ∈ S. Since (P_{i}, Q_{i}) ∈ S (i = 1, 2), there are some H_{i} such that P_{i} ≡ H_{i}{μX.E/X} and Q_{i} ≡ H_{i}{μX.F/X}. So (P′, Q′) ∈ S.

Case 4 G ≡ G_{1} + G_{2}, G ≡ G′\a or G ≡ G′[S].

All these cases are similar to case 3.

Case 5 G ≡ μY.G′.

(1) Y ≡ X. Then X is not a free process variable of G and both G{μX.E/X} and G{μX.F/X} are just μY.G′. Clearly (P′, P′) ∈ S.

(2) Y ≢ X. Then G{μX.E/X} ≡ μY (G′{μX.E/X}) and μY (G′{μX.E/X})⟶_{u}P′. Thus

G′{μY.G′/Y }{μX.E/X}⟶_{u}P′

where G′{μY.G′/Y }{μX.E/X} ≡ G′{μX.E/X}{μY.(G′{μX.E/X})/Y }. By induction, G′{μY.G′/Y }{μX.F/X}⟶_{u}Q′′ with Q′ ∼ Q′′ and (P′, Q′) ∈ S. Hence, μY.G′{μX.F/X}⟶_{u}Q′′ with Q′ ∼ Q′′ and (P′, Q′) ∈ S.

2. Suppose G{μX.E/X}⟶^{α}_{u}P′. Similar to 1. □

4.3 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.8 A process variable X is weakly guarded in E if every occurrence of X is within some subterm α(t)_{e}^{e′}. F of E.

Definition 4.9 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.14 For any process E, which is closed with respect to time variables, 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 form E′{P⃗ /X⃗} for some process E′. Further-

more, for any agents Q⃗, E{Q⃗/X⃗}⟶^{α}_{u}E′{Q⃗/X⃗} (or E{Q⃗/X⃗}⟶^{α}_{u}E′{Q⃗/X⃗}).

Proof We proceed by transition induction on the depth of the inference of

E{P⃗ /X⃗}⟶^{α}_{u}P′ and E{P⃗ /X⃗}⟶_{u}P′.

1. Suppose E{P⃗ /X⃗}⟶^{α}_{u}P′. Consider the cases for E.

Case 1 E ≡ Y.

Since process variables X⃗ are weakly guarded in E, Y is not in X⃗ and Y {P⃗ /X⃗} ≡ Y has no derivatives. This case is impossible.

Case 2 E ≡ α(t)_{v}^{v′}. F Then v ≤ u ≤ v′ and P′ ≡ F {P⃗ /X⃗}{u/t}. Since P⃗ are agents, we have

F {P⃗ /X⃗}{u/t} ≡ F {u/t}{P⃗ /X⃗}

Also, for any agents Q⃗,

E{Q⃗/X⃗} ≡ α(t)_{v}^{v′}. (F {Q⃗/X⃗})⟶^{α}_{u}F {Q⃗/X⃗}{u/t}

and

F {Q⃗/X⃗}{u/t} ≡ F {u/t}{Q⃗/X⃗}

Case 3 E ≡ E_{1} + E_{2}

Then E_{1}{P⃗ /X⃗}⟶^{α}_{u}P′ or E_{2}{P⃗ /X⃗}⟶^{α}_{u}P′. Suppose E_{1}{P⃗ /X⃗}⟶^{α}_{u}P′.

By induction, P′ has the form E′{P⃗ /X⃗} and for any agents Q⃗,

E_{1}{Q⃗/X⃗}⟶^{α}_{u}E′{Q⃗/X⃗}

So, E{Q⃗/X⃗}⟶^{α}_{u}E′{Q⃗/X⃗}. The other case is similar.

Case 4 E ≡ E_{1} | E_{2}

Subcase 4.1 E_{1}{P⃗ /X⃗}⟶^{α}_{u}P_{1}, E_{2}{P⃗ /X⃗}⟶_{u}P_{2} and P′ ≡ P_{1} | P_{2}. By

induction, P_{1} ≡ E′_{1}{P⃗ /X⃗}, P_{2} ≡ E′_{2}{P⃗ /X⃗} for some E′_{1}, E′_{2}, and for

any agents Q⃗, E_{1}{Q⃗/X⃗}⟶^{α}_{u}E′_{1}{Q⃗/X⃗}, E_{2}{Q⃗/X⃗}⟶_{u}E′_{2}{Q⃗/X⃗}. Hence,

P′ ≡ (E′_{1} | E′_{2}){P⃗ /X⃗} and E{Q⃗/X⃗}⟶^{α}_{u}(E′_{1} | E′_{2}){Q⃗/X⃗}.

Subcase 4.2 E_{1}{P⃗ /X⃗}⟶_{u}P_{1}, E_{2}{P⃗ /X⃗}⟶^{α}_{u}P_{2} and P′ ≡ P_{1} | P_{2}. Sam-

ilar to case 4.1.

Subcase 4.3 α = τ, E_{1}{P⃗ /X⃗}⟶^{a}_{u}P_{1}, E_{2}{P⃗ /X⃗}⟶^{ā}_{u}P_{2} and P′ ≡ P_{1} | P_{2}.

Similar to case 4.1.

Case 5 E ≡ F \a or E ≡ F [S]. Similar to case 4.

2. Suppose E{P⃗ /X⃗}⟶_{u}P′. Similar to 1. □

Lemma 4.15 For any process E which contain 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}.

The result follows directly from the definition of maximal delay time of processes.

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

Proposition 4.16 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_{i} (i ∈ I). Then

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

Proof Suppose P⃗ ∼ E⃗{P⃗ /X⃗} and Q⃗ ∼ E⃗{Q⃗/X⃗}. We want to prove P_{i} ∼ Q_{i} (i ∈ I), and this follows by taking E ≡ X_{i}, if we can show that

S = {(E{P⃗ /X⃗}, E{Q⃗/X⃗}) | fpv(E) ⊆ X⃗ and ftv(E) = ∅}

is a strong T -bisimulation up to ∼.

1. Suppose E{P⃗ /X⃗}⟶^{α}_{u}P′. Consider the cases for E.

Case 1 E = X_{i}

Then E{P⃗ /X⃗} ≡ P_{i}⟶^{α}_{u}P′ and E_{i}{P⃗ /X⃗}⟶^{α}_{u}P′′ ∼ P′ (P_{i} ∼ E_{i}{P⃗ /X⃗}).

By the lemma, P′′ ≡ E′{P⃗ /X⃗} and E_{i}{Q⃗/X⃗}⟶^{α}_{u}E′{Q⃗/X⃗}. But E{Q⃗/X⃗} ≡

Q_{i} ∼ E_{i}{Q⃗/X⃗}, so E{Q⃗/X⃗}⟶^{α}_{u}Q′ ∼ E′{Q⃗/X⃗}. Hence P′ ∼ S ∼ Q′. and

P′ ∼ Q′.

Case 2 E ≡ α(t)_{v}^{v′}. F.

Then v ≤ u ≤ v′ and P′ ≡ F {P⃗ /X⃗}{u/t}. Since all P⃗ are agents, we

have P′ ≡ F {u/t}{P⃗ /X⃗}. Also E{Q⃗/X⃗} ≡ α(t)_{v}^{v′}. F {Q⃗/X⃗}⟶^{α}_{u}Q′, where

Q′ ≡ F {Q⃗/X⃗}{u/t} ≡ F {u/t}{Q⃗/X⃗}. Hence (P′, Q′) ∈ S.

Case 3 E ≡ E_{1} + E_{2}, E ≡ E_{1} | E_{2}, E ≡ F \a and E ≡ F [S]. All these cases are similar.

2. Suppose E{P⃗ /X⃗}⟶^{α}_{u}P′. Similar to 1.

3. |E{P⃗ /X⃗}|_{T} = |E{Q⃗/X⃗}|_{T} (by the lemma). □

Now we are in the position of showing that for any guarded equations X⃗ = E⃗, they have a solution, i.e. there are agents P⃗ such that P⃗ ∼ E⃗{P⃗ /X⃗}.

Proposition 4.17 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⃗ be weakly guarded in every E_{i}, then there are some agents P⃗ such that

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

Proof By induction on the number m of equations in X⃗ = E⃗.

Case 1 m = 1. Then there is a single equation X = E, where E contains at most free process variable X and is closed with respect to time variables. Clearly, agent μX.E is a solution of X = E.

Case 2 For m + 1 equations X⃗ = E⃗, x_{n+1} = E_{n+1}, we have

X⃗ = E⃗{μX_{n+1}.E_{n+1}/X_{n+1}}

By induction, there are m agents P⃗ such that

P⃗ ∼ E⃗{μX_{n+1}.E_{n+1}/X_{n+1}}{P⃗ /X⃗}

Also, equation X_{m+1} = E_{m+1}{P⃗ /X⃗} has a solution

P_{n+1} = μX_{m+1}.E_{m+1}{P⃗ /X⃗}

Clearly, P⃗, P_{m+1} are agents which we are looking for. □

Therefore, any weakly guarded equations X⃗ = E⃗, where E⃗ are closed with respect to time variables and contain at most free process variables X⃗, have an unique solution up to strong equivalence.

Corollary 4.18 (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.4 Decidability

In this section, we only consider finite processes, i.e. those without recursion and constants.

For any process P, there is a normal form P′ (by using the above laws) such that P ∼ P′′. In the sequel of this section, we suppose every process is in normal form.

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

Definition 4.11 A formula A is said to be the weakest condition for P to be bisimilar to Q if A ⊧ P ∼ Q and B ⊧ P ∼ Q implies B → A.

Proposition 4.19 If A is the weakest condition for P to be bisimilar to Q, then

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

For any processes P and Q, we construct W C(P, Q), the weakest condition for P to be bisimilar to Q.

Definition 4.12 For any processes P and Q, where

P ≡ ∑_{i∈I} a_{i}(t_{i})_{e_{i}}^{e′_{i}}. P_{i} + (e)δ

and

Q ≡ ∑_{j∈J} b_{j}(s_{j})_{f_{j}}^{f′_{j}}. Q_{j} + (f)δ

let W C(P, Q) = (e = f) ⋀

⋀_{i∈I}(∀t(max(0, e_{i}) ≤ t ⋀ t ≤ e′_{i} → ⋁_{j∈J^{a_{i}=b_{j}}}(f_{j} ≤ t ⋀ t ≤ f′_{j} ⋀ W C(P_{i}{t/t_{i}}, Q_{j}{t/s_{j}})))))

⋀_{j∈J}(∀s(max(0, f_{j}) ≤ s ⋀ s ≤ f′_{j} → ⋁_{i∈I^{a_{i}=b_{j}}}(e_{i} ≤ s ⋀ s ≤ e′_{i} ⋀ W C(P_{i}{s/t_{i}}, Q_{j}{s/s_{j}}))))

where t, s are some fresh variables.

We show that the formula W C(P, Q) is the weakest condition for P to be bisimilar to Q.

Proposition 4.20 For any processes P and Q, W C(P, Q) is the weakest condition for P to be bisimilar to Q.

The proof can be found in [Che91b].

Corollary 4.21 For any processes P and Q, W C(P, Q) if and only if P ∼ Q.

For any time expression e over (T ⋃{∞}, ≤), we have e ≤ ∞. For any processes P and Q, we can replace terms of the form e ≤ ∞ by 0 = 0 throughout W C(P, Q).

Definition 4.13 So for any processes P and Q, let W C^{∗}(P, Q) be the result of substituting all terms of form e ≤ ∞ by 0 = 0 in W C(P, Q).

Lemma 4.22 For any processes P and Q, W C(P, Q) if and only if W C^{∗}(P, Q).

Lemma 4.23 For any processes P and Q which contain at most time variables (t_{1}, …, t_{n}),

P ∼ Q if and only if ∀t_{1} … ∀t_{n}W C^{∗}(P, Q)

If the time domain is (N ⋃{∞}, ≤), then for any processes P and Q which contain at most free time variables (t_{1}, ⋯, t_{n}), ∀t_{1} ⋯ ∀t_{n}.W C^{∗}(P, Q) is a sentence of the first order theory (N, +).

Theorem 4.24 ∼ is decidable over time domain (N ⋃{∞}, ≤).

The result follows from the decidability of the first-order theory of the integers with +. Since the first-order theory of the integers with + and ×, i.e. Th(N, +, ×), is undecidable, this justifies our decisions in the choice of time expressions.

If the time domain is (R ⋃{∞}, ≤), then for any processes P and Q which contain at most free time variables (t_{1}, ⋯, t_{n}), ∀t_{1} ⋯ ∀t_{n}.W C^{∗}(P, Q) is a sentence of the first order theory (R, +, ×).

Theorem 4.25 ∼ is decidable over dense time domain (R ⋃{∞}, ≤).

The result follows from the decidability of the first-order theory of the reals with + and × (Tarski, 1948).

5 Behavoiur Abstraction in Timed Processes

5.1 Weak Bisimulation

The 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 must be matched by a τ action of the other. In this section, we define a weak equivalence which allows a τ action to be matched by zero or more τ actions.

Definition 5.1 We say P ⟹^{ϵ}_{u}P′ if P ⟶^{τ}_{u_{1}} ⋯ ⟶^{τ}_{u_{n}}·⟶_{v}P′ for some u_{1}, …, u_{n}, v

∈ T such that u = v + u_{1} + ⋯ + u_{n}.

Since the internal action τ is not observable, an agent which performs some τ actions during time u can not be distinguished from an agent which just idles time u without any action, including τ actions. Thus P ⟹^{ϵ}_{u}P′ means that process P idles time u without any observable actions.

Definition 5.2 We say P ⟹^{a}_{u}P′ if P ⟹^{ϵ}_{v} · ⟶^{a}_{w} · (⟶^{τ}_{0})^{∗}P′ for some v, w ∈ T such that u = v + w.

Transition P ⟹^{a}_{u}P′ means that an action a is observed at time u. However, before action a, there may be many (but finite) unobservable actions, i.e. τ actions. Also there may be many (but finite) internal actions happening at the same time as action a.

Notation α̂ =^{def} if α = τ then ϵ else α

Definition 5.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 there is a Q′ such that Q⟹^{α̂}_{u}Q′ and (P′, Q′) ∈ R.

2 if P ⟶_{u}P′, then there is a Q′ such that Q⟹^{ϵ}_{u}Q′ and (P′, Q′) ∈ R.

3 if Q⟶^{α}_{u}Q′, then there is a P′ such that P ⟹^{α̂}_{u}P′ and (P′, Q′) ∈ R.

4 if Q⟶_{u}Q′, then there is a P′ such that P ⟹^{ϵ}_{u}P′ and (P′, Q′) ∈ R.

We say two agents P and Q are weak bisimilar if there is a weak bisimulation R such that (P, Q) ∈ R.

Definition 5.4 ≈ = ⋃{R | R is a weak bisimulation}

Proposition 5.1 ≈ is the largest weak bisimulation. Moreover ≈ is an equivalence relation.

The proof is similar to that for strong bisimulation.

Proposition 5.2 P ∼ Q implies P ≈ Q

The proof follows directly from the definitions of strong and weak bisimulations. All laws for strong equivalence still hold for weak equivalence.

Proposition 5.3

1 τ(t)_{e}^{e′}. (t >> (e)P) + (e)P ≈ τ(t)_{e}^{e′}. (t >> (e)P), where e ≤ e′ and t ∉ ftv(P).

2 Q + τ(t)_{e}^{e′}. (t >> (e)P) + (e)P ≈ Q + τ(t)_{e}^{e′}. (t >> (e)P), where |Q|_{T} ≤ e ≤ e′ and t ∉ ftv(P).

3 τ(t)_{e}^{e′}. (t >> ((e)P +(e′)δ)) ≈ (e)P +(e′)δ, where e ≤ e′ and t ∉ ftv((e)P +(e′)δ).

4 Q + τ(t)_{e}^{e′}. (t >> ((e)P + (e′)δ) ≈ Q + (e)P + (e′)δ, where |Q|_{T} < e ≤ e′ and t ∉ ftv((e)P + (e′)δ).

Proof All properties may be proved by exhibiting appropriate weak bisimulations. For (3), it only needs to show that

{(τ(t)_{e}^{e′}. (t >> ((e)P + (e′)δ)), (e)P + (e′)δ) | t ∉ ftv((e)P + (e′)δ)}

is a weak bisimulation. □

Similar to CCS, weak equivalence is not a congruence relation. In general, it does not preserve summation. For example, τ(t)_{2}^{8}. nil ≈ nil, but τ(t)_{2}^{8}. nil + a(s)_{8}^{∞}. nil ≉ nil + a(s)_{8}^{∞}. nil. The right hand side may always perform action a, but the left hand side may reject action a. However, weak equivalence is preserved by the other operations.

Proposition 5.4 For any agents P and Q, P ≈ Q implies

1 α(t)_{e}^{e′}. P ≈ α(t)_{e}^{e′}. Q

2 P | R ≈ Q | R

3 P \a ≈ Q\a

4 P [S] ≈ Q[S]

All properties may be proved by exhibiting appropriate weak bisimulations. As with strong bisimulation, we may also generalize weak bisimulation to processes.

5.2 Observational Congruence

Weak equivalence is not fully substitutive. In general, it is not preserved by nondeterministic choice. In this section, we define an equality which will be fully substitutive and also the largest congruence relation included by ≈.

Definition 5.5 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 5.5 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 is direct (by taking P ≡ δ in the definition of =^{+}).

The converse of the above does not hold. For example, τ(t)_{0}^{0}. .nil ≈ nil, but τ(t)_{0}^{0}. .nil ≠^{+} nil. Also a(t)_{2}^{10}. τ(s)_{0}^{0}. nil =^{+} a(t)_{2}^{10}. nil, but a(t)_{2}^{10}. τ(s)_{0}^{0}. nil ≁ a(t)_{2}^{10}. nil.

We say an agent P is stable if P cannot perform an internal action τ as its first action.

Definition 5.6 An agent P is stable if for any u ∈ T and any P′ ∈ P, P −̸→^{τ}_{u} P′.

Proposition 5.6 For any stable agents P and Q, P ≈ Q implies P =^{+} Q

Proof We only need to show that

{(P + R, Q + R) | P ≈ Q and P, Q stable} ⋃ ≈

is a weak bisimulation.

Proposition 5.7 P ≈ Q implies α(t)_{e}^{e′}. P =^{+} α(t)_{e}^{e′}. Q.

Proof We only need to show that

{(α(t)_{e}^{e′}. P + R, α(t)_{e}^{e′}. Q + R) | P ≈ Q} ⋃ ≈

is a weak bisimulation.

Proposition 5.8 (τ-Laws)

1 τ(t)_{0}^{e′}. (α(s)_{0}^{0}. P + Q) =^{+} α(s)_{0}^{0}. (P {0/t}) + τ(t)_{0}^{e′}. (α(s)_{0}^{0}. P + Q) e′ ≥ 0

2 α(t)_{e}^{e′}. (τ(s)_{0}^{0}. P + Q) =^{+} α(t)_{e}^{e′}. (P {0/s}) + α(t)_{e}^{e′}. (τ(s)_{0}^{0}. P + Q)

3 α(t)_{f}^{f′}. (Q+τ(s)_{e}^{e′}. (t >> (e)P)+(e)P) =^{+} α(t)_{f}^{f′}. (Q+τ(s)_{e}^{e′}. (t >> (e)P)), where |Q|_{T} ≤ e ≤ e′ and t ∉ ftv(P).

4 α(t)_{f}^{f′}. (Q + τ(s)_{e}^{e′}. (t >> ((e)P + (e′)δ))) =^{+} α(t)_{f}^{f′}. (Q + (e)P + (e′)δ), where |Q|_{T} < e ≤ e′ and s ∉ ftv((e)P + (e′)δ).

(1) and (2) may be proved be showing appropriate weak bisimulations. (3) and (4) follow from the properties of weak bisimulation and the above property.

We can also give an alternative definition of =^{+} in the style of bisimulation. To do so, we first define an equivalence =^{c} and then show that =^{+} and =^{c} coincide.

Definition 5.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) symmetric to (1) and (2).

Definition 5.8 =^{c} =^{def} ⋃{R | R is a C−bisimulation}.

Proposition 5.9 For any agents P and Q, P =^{c} Q if and only if P =^{+} Q.

Proof (⇒) It is enough to show that

{(P + R, Q + R) | P =^{c} Q}

is a weak bisimulation. (⇐) Suppose P ≠^{c} Q and for any a ∈ Act, u ∈ T

Case 1 P ⟶_{u} · ⟶^{α}_{0}, 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 should 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′.

Case 2 P ⟶_{u}P′, but |Q|_{T} < u.

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.

All other cases are similar. □

The equivalence =^{+} is fully substitutive, as shown by the following propositions.

Proposition 5.10 For any processes E and F, E =^{+} F implies

1 α(t)_{e}^{e′}. E =^{+} α(t)_{e}^{e′}. F

2 E + G =^{+} F + G

3 E | G =^{+} F | G

4 E\a =^{+} F \a

5 E[S] =^{+} F [S]

All of these properties may be proved by showing appropriate C-bisimulations.

Proposition 5.11 For any processes E⃗ and F⃗ which contain at most process variables X⃗, E⃗ =^{+} F⃗ implies μX⃗.E⃗ =^{+} μX⃗.F⃗.

Proof For simplicity, we only consider one equation. Let E and F be closed with respect to time variables and contain at most free process variable X. Suppose E =^{+} F. By showing that

S =^{def} {(G{μX.E/X}, G{μX.F/X}) | ftv(G) = and fpv(G) ⊆ {X}}

is a weak bisimulation up to ≈, we can establish μX.E ≈ μX.F (by taking G ≡ X). To achieve μX.E =^{+} μX.F, we need to prove that S has the following properties:

(1) If G{μX.E/X}⟶^{α}_{0}P′, then G{μX.F/X}⟹^{α}_{0}Q′ and P′ ≈ ·S· ≈ Q′ for

some Q′.

(2) If G{μX.E/X}⟶_{u}P′, then G{μX.F/X}⟶_{u}Q′ and P′ ∼ ·S· ∼ Q′ for some Q′.

The above two properties may be proved by induction on the inferences. Clearly, these two properties make S to be a weak bisimulation up to ≈. Hence P′ ≈ ·S· ≈ Q′ implies P′ ≈ Q′. By choosing G ≡ X, we have μX.E =^{+} μX.F. Note that if S is a C-bisimulation, then ∼ ·S· ∼ is also a C-bisimulation. □

5.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 5.9 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 5.10 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 that equations X⃗ = E⃗ are guarded (sequential) if all X⃗ are guarded (sequential) in E⃗. Similar to weak guardedness, the guardedness ensures that process variables cannot affect the first non-τ action.

Lemma 5.12 Let E be guarded, sequential and closed with respect to time variables, containing at most free process variable X⃗. If E{P⃗ /X⃗}⟶^{α}_{u}P′, then there is a process H such that P′ ≡ H{P⃗ /X⃗} and for any agents Q⃗, E{Q⃗/X⃗}⟶^{α}_{u}H{P⃗ /X⃗}. Moreover H is sequential and contains at most free process variables X⃗. Also 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 Constant, a Composition, a Restriction or a Relabelling, then it contains no free process variables and the result is immediate. 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⃗, there is a unique solution up to observational congruence.

Proposition 5.13 Let E⃗ be guarded and sequential processes which are closed with respect to time variable and contain at most free process variables X⃗,

P⃗ =^{+} E⃗{P⃗ /X⃗} and Q⃗ =^{+} E⃗{Q⃗/X⃗} implies P⃗ =^{+} Q⃗

Proof For simplicity, we only consider one equation X = E. Suppose P =^{+} E{P/X} and Q =^{+} E{Q/X}. Let

S =^{def} {(G{P/X}, G{Q/X}) | ftv(G) = ∅ and fpv(G) ⊆ {X} and G sequential}

If we can show that S has the properties:

(1) If G{P/X}⟶^{α}_{0}P′, then G{Q/X}⟹^{α}_{0}Q′ and P′ ≈ ·S· ≈ Q′ for some Q′.

(2) If G{P/X}⟶_{u}P′, then G{Q/X}⟶_{u}Q′ and P′ ∼ ·S· ∼ Q′ for some Q′.

then, by symmetric arguments and by taking G ≡ X, we have the result P =^{+} Q.

To prove (1), we first show that if G{P/X}⟹^{ϵ}_{0}P′, then G{Q/X}⟹^{ϵ}_{0}Q′ and

P′ ≈ ·S· ≈ Q′ for some Q′. Suppose G{P/X}⟹^{ϵ}_{0}P′. Since G{P/X} =^{+}

G{E{P/X}/X} (substitutivity of equality), we have

G{E{P/X}/X}⟹^{ϵ}_{0}P′′ ≈ P′ for some P′′

But G{E/X} is guarded and sequential, by the above lemma there is a sequential G′ such that

P′′ ≡ G′{P/X} and (G{E/X}){P/X}⟹^{ϵ}_{0}G′{Q/X}

Also G{Q/X} =^{+} G{E{P/X}/X} ≡ (G{E/X}){P/X}, we have

G{Q/X}⟹^{ϵ}_{0}Q′ ≈ G′{Q/X} for some Q′

Hence, P′ ≈ G′{P/X}SG′{Q/X} ≈ Q′. Now suppose G{P/X}⟶^{α}_{0}P′. Then

(G{E/X}){P/X}⟹^{ϵ}_{0} · ⟶^{α}_{0}⟹^{ϵ}_{0}P′′ ≈ P′

By applying the above lemma repeatedly, we have a sequential G′ such that

(G{E/X}){P/X}⟹^{ϵ}_{0} · ⟶^{α}_{0}G′{P/X}⟹^{ϵ}_{0}P′′ ≈ P′

and

(G{E/X}){Q/X}⟹^{ϵ}_{0} · ⟶^{α}_{0}G′{Q/X}

Hence

G′{Q/X}⟹^{ϵ}_{0}Q′′ with P′′ ≈ ·S· ≈ Q′′

and

G{Q/X}⟹^{α}_{0}Q′ ≈ Q′′

So

P′ ≈ ·S· ≈ Q′

The proof of (2) is similar to that for strong equivalence. □

Proposition 5.14 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⃗ are guarded and sequential in every E_{i} (i ∈ I). Then there are some agents P⃗ such that

P⃗ =^{+} E⃗{P⃗ /X⃗}

The proof is similar to that for strong equivalence.

Corollary 5.15 (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⃗}

6 Conclusion

In this paper, we propose a general interleaving model for real-time systems. We make no assumption about the underlying nature of time allowing time to be discrete (such as the integers) or dense (such as the rationals and the reals). We also make no assumption of the Maximal Progress Principle. The time variables of the language allow us to represent the notion of time dependency and the language is therefore more expressive than those without time variables. We extend the notion of bisimulation to timed processes. Strong equivalence over finite timed processes, those processes without recursion, is still decidable and the decidability is independent of the choice of time domain. In [Che91b], we also present a sound and complete proof system for strong equivalence over finite processes. The proof system is finite in the sense that there are no infinite proof rules. Therefore the proof system is of practical significance.

The works such as [HR90, Gro90, Sif90] are only for discrete time and therefore cannot express the notion of time dependency. The works in [BB91, CAM90, MT90, Wan90] all make no assumption of the underlying nature of time. However, the works in [CAM90, Wan90] are based on an assumption of the maximal progress principle. There are not time variables in Moller and Tofts’ TCCS [MT90] and it cannot express the notion of time dependency. There is no expansion law over dense time in TCCS. Maybe this is why some people misunderstand that TCCS is only for the discrete time. Baeten and Bergstra’s ACPρI is on a different process algebra ACP and has a notion of integration which can be seen as an alternative composition over a continuum of alternatives. It is more general than our Timed CCS. However, to get the completeness result, Klusener [Klu91] had to introduce some machinery, such as basic terms and condition terms, and restrict to a sublanguage which only allows “prefixed integration”. In fact, this restricted sublanguage just corresponds to our Timed CCS. Klusener’s proof system contains some infinite proof rules and is for absolute time, not for relative time. The approach of [Che91b] may also be used to the restricted language of ACPρI.

As future work, we may consider proof systems for strong equivalence over regular processes, i.e. the processes which may contain recursion. Also, we may consider proof systems for weak equivalence.

Acknowledgements: I would like to thank S. Anderson for suggesting me to study timed calculi and also many helpful discussions and comments, to F. Moller for many helpful discussions about timed calculi and also useful comments, to J. Power for many helpful discussions and suggestions on the models of timed processes, to M. Jerrum for interesting discussions on the decidability of strong equivalence.

References

[BB91] J.C.M. Baeten and J.A. Bergstra(1991), Real Time Process Algebra, Formal Aspects of Computing, 3(2), pp142-188

[BKR86] M. Ben-Or, D. Kozen and J. Reif(1986), The Complexity of Elementary Algebra and Geometry, Journal of Computer and System Sciences, 32, pp 251-264

[BK84] J.A. Bergstra and J.W. Klop(1984), Process Algebra for Synchronous Communication, Information and Control 60(1-3), pp. 109-137

[BK85] J.A. Bergstra and J.W. Klop(1985), Algebra of Communicating Processes with Abstraction, Theoretical Computer Science 37, pp. 77-121

[Che91a] L. Chen(1991), Specification and Verification of Real-Time Systems, Draft Note.

[Che91b] L. Chen(1991), Decidability and Completeness in Real-Time Processes, Technical Report ECS-LFCS-91-185, Edinburgh University

[Che91c] L. Chen(1991), Timed Synchronization Trees, Draft, LFCS, Edinburgh University

[CAM90] L. Chen, S. Anderson and F. Moller(1990), A Timed Calculus of Communicating System, Technical Report ECS-LFCS-90-127, University of Edinburgh

[Col75] G. E. Collins(1975), Quantifer Elimination for Real Closed Fields by Cylindric Algebraic Decomposition, in Proc. 2nd GI Conference on Automata Theory and Formal Language, pp 134-183.

[End72] H. B. Enderton(1972), A Mathematical Introduction to Logic, Academic Press, Inc.

[Gro90] J.F. Groote(1990), Specification and Verification of Real Time Systems in ACP, Report CS-R9015, CWI, Amsterdam

[HR90] M. Hennessy and T. Regan(1990), A Temporal Process Algebra, Technical Report 2/90 University of Sussex

[Hoa85] C.A.R. Hoare(1985), Communicating Sequential Processes, Prentice-Hall international [Klu91] A.S. Klusener(1991), Completeness in Real Time Process Algebra, Pro-

ceedings of CONCUR’91, Lecture Notes in Computer Science 527, pp96-110

[Mil80] R. Milner(1980), A Calculus of Communicating systems, Lecture Notes in Computer Science 92, Springer-verlag

[Mil83] R. Milner(1983), Calculi for Synchrony and Asynchrony, Theoretical Computer Science, 25, pp 267-310

[Mil89] R. Milner(1989), Communication and Concurrency, Prentice-Hall international

[MT90] F. Moller and C. Tofts(1990), A Temporal Calculus of Communicating System, Lecture Notes in Computer Science 458, pp 401-415

[MT91] F. Moller and C. Tofts(1991), Relating Processes With Respect to Speed, Technical Report ECS-LFCS-91-143, University of Edinburgh

[Sif90] X. Nicollin, J. Richier, J. Sifakis and J. Voiron(1990), ATP : an Algebra for Timed Processes, Laboratoire de Genie Informatique, IMAG-Campus, 38041 Grenoble Cedex, France

[Par81] D.M.R. Park(1981), Concurrency and Automata on Infinite Sequences, Lecture Notes in Computer Science 104, Springer-Verlag

[Plo81] G.D. Plotkin(1981), A Structured Approach to Operational Semantics, DAIMI FN-19, Computer Science Department, Arhus University, Denmark

[RR88] R. Reed and A. W. Roscoe(1988), A Timed Model for Communicating Sequential Processes, Theoretical Computer Science, 58, pp 249-261

[Wan90] Y. Wang(1990), Real-time Behaviour of Asynchronous Agents, Lecture Notes in Computer Science 458, pp 502-520