BRICS RS-96-8 Hansen et al.: Bisimulations for Asynchronous Mobile Processes

BRICS

Basic Research in Computer Science

Bisimulations for Asynchronous Mobile Processes

Martin Hansen Hans H� uttel Josva Kleist

BRICS Report Series RS-96-8 ISSN 0909-0878 April 1996 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1996, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

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

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

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

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

BRICS publications are in general accessible through WWW and anonymous FTP:

http://www.brics.dk/
ftp ftp.brics.dk (cd pub/BRICS)

Bisimulations for asynchronous mobile processes

Martin Hansen  Hans Hüttel  Josva Kleist
BRICS^{∗}

Department of Computer Science University of Aalborg Fredrik Bajersvej 7E, 9220 Aalborg Ø, Denmark

Abstract

Within the past few years there has been renewed interest in the study of value-passing process calculi as a consequence of the emergence of the π-calculus. Here, [MPW89] have determined two variants of the notion of bisimulation, late and early bisimilarity. Most recently [San93] has proposed the new notion of open bisimulation equivalence.

In this paper we consider Plain LAL, a mobile process calculus which differs from the π-calculus in the sense that the communication of data values happens asynchronously. The surprising result is that in the presence of asynchrony, the open, late and early bisimulation equivalences coincide – this in contrast to the π–calculus where they are distinct. The result allows us to formulate a common equational theory which is sound and complete for finite terms of Plain LAL.

1 Introduction

An important question in the theory of process calculi is when two processes can be said to exhibit the same behaviour and a number of behavioural equivalences have been proposed. Traditionally, the emphasis has been on studying the equivalences for ‘pure’ processes where communication does not involve the passing of data values. However, within the past few years there has been renewed interest in the study of value-passing as a consequence of the emergence of the π-calculus. Here [MPW89] have determined two variants of the notion of bisimulation, late and early bisimilarity, differing in the assumption of when a data value is instantiated. Most recently [San93] has proposed a new notion of bisimulation equivalence which he calls open bisimilarity. Sangiorgi formulates a sound and complete equational theory for open bisimilarity on finite (i.e. non-recursive) π-calculus terms.

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

An important theorem is that the three notions of bisimilarity are distinct within the π-calculus, with open bisimulation being strictly finer than late bisimulation which in turn is strictly finer than early bisimulation. The late/early distinction has been studied for the much coarser testing equivalence of Hennessy and De Nicola and it has been shown by [Ing94] and [BN92] that the late and early testing equivalences coincide, both for a process calculus with simple data values and conditional expression and for the π-calculus.

In this paper we consider Plain LAL, a mobile process calculus which differs from the π-calculus in the sense that the communication of data values happens asynchronously. Previously, [HT91] and [Bou92] have described so-called asynchronous π-calculi. In [Ode95] it is shown how familiar programming constructs can be encoded in a straightforward fashion within an asynchronous π-calculus, thus confirming the naturalness of the combination of asynchrony and mobility.

The main result of the present paper is that in the presence of asynchrony, the open, late and early bisimulation equivalences coincide. A related results was established by [HY93]; however this result was shown for another asynchronous calculus, the simpler so-called γ-calculus. As the equivalences are one and the same in Plain LAL, this leads us to formulate an equational theory which is sound for finite terms of Plain LAL. Most proofs of theorems have been omitted; they can be found in [HK94].

2 Plain LAL

The process calculus that we shall consider here uses a notion of asynchrony inspired by the Linda paradigm for parallel programming proposed by [GB82]. In Linda, a program is viewed as a collection of concurrent processes and data (‘tuples’) existing in a common ‘tuple space’. Tuples communicate by depositing tuples in the ‘tuple space’ by using the out and eval operators and retrieving them using the rd and in operators. When retrieving another tuple, a Linda tuple can specify which kinds of tuples that may be retrieved by means of a notion of pattern matching.

Plain LAL is a two-level calculus as we distinguish between processes and systems. Processes correspond to tuples in a Linda ‘tuple space’ and are deposited by a spawn operator at the level of processes. This is the only means of introducing parallelism; Plain LAL has no explicit parallel composition operator for processes and is in this respect similar not only to out and eval operators of Linda, but also to the fork calculus of [Hav94] and to notions underlying the semantics of applicative languages with concurrency, such as Concurrent ML ([BMT92]).

The pattern matching of Linda used to retrieve tuples is modelled by Plain LAL processes having names. A Plain LAL agent (or system) S, T, … ∈ Agent is the parallel composition of a set of named processes, each of the form (α, P) where α, β, γ … ∈ Name range over names and P, Q, … ∈ Proc range over processes. The only data that can be communicated in Plain LAL are names; a process (α, P) can obtain the name γ from another process (β, γ) via the name β, called the location of γ.

2.1 Syntax

Expressions in Plain LAL are given by the following syntax:

\begin{aligned}S & ::= & (α, P) | (α)S | S_{1}|S_{2} | • \\ P & ::= & ∑_{i∈I}a_{i}.P_{i} | (α)P | α | ξ(P) \\ a & ::= & α!P | α?β | τ \end{aligned}

The chief operators of Plain LAL are the prefixing operators. In Plain LAL, the ‘output’ prefix α!P assumes the role of the spawn operator – it creates a parallel component (α, P), i.e. a process P located at α. The ‘input’ prefix α?β asks for a name from any parallel component whose location is α and binds the name to β. The τ prefix denotes silent moves.

Names can be made local using the restriction operator; (α)S denotes that α is a name local to S. We define (L)P resp. (L)S where L ⊆ Name as P resp. S restricted by all names in L. Input prefixing and restriction work as binding operators on names and give rise to the familiar definitions of free and bound names.

Processes can be built using sums of prefixed processes, restriction and values α. ξ(P) is the replication operator of the π-calculus; we need this to be able to express infinite behaviours (alternatively, we could have added a recursion operator to the syntax; the two notions are inter-expressible.)

Systems are the parallel composition of processes and can themselves be composed in parallel. We let Π_{i∈I}S_{i} denote the parallel composition of a number of systems where I is an index set. In the rest of this paper, we shall assume that any such index set is finite; we sometimes omit the index set and indices when they are clear from the context. We write 0 for ∑_{∅} a.P and a for a.0; further we use + for binary sum.

2.2 Semantics

Our operational semantics for Plain LAL consists of three levels: The basis is a commitment semantics for processes which describes which actions processes can commit to. At the system level we have a labelled transition system which, based on the commitments of the processes, controls which interactions can occur. To simplify the rules we have a structural congruence which lets us manipulate agents by their structure.

The commitment semantics for processes is given by:

[action_{≻}] a.P ≻ a.P
[sum_{≻}] \frac{P_{j} ≻ a.P}{∑_{I} P_{i} ≻ a.P} if j ∈ I
[res_{≻}]  \frac{P ≻ a.P′}{(α)P ≻ a.(α)P′} if α ∉ fn(a)

The structural congruence ≡ is defined as the smallest congruence relation satisfying:

S ≡ T if S and T are α-convertible
(α)(β, 0) ≡ (β, 0)
(α, 0) ≡ •
(β)(α)S ≡ (α)(β)S
(α)((β, P)|(γ, Q)) ≡ (α)(β, P)|(γ, Q) if α ∉ fn(Q) ∪ {γ}
(α, (β)P) ≡ (β)(α, P) if α ≠ β
(α, ξ(P)) ≡ (α.P)|(α, ξ(P))

(S/ ≡, |, •) is a symmetric monoid

Finally, the labelled transition system takes labels m ∈ Label given by the following syntax:

[input]  \frac{P ≻ α?β.P′}{(α, P) \overline{}^{α?β} (α, P′)}
[value]  (α, β) \overline{}^{β@α} •
[open]  \frac{S \overline{}^{β@α} S′}{(β)S \overline{}^{(β)@α} S′}

[com_{1}]  \frac{S \overline{}^{β@α} S′ T \overline{}^{α?γ} T′}{S|T \overline{}^{τ} S′|T′\{^{β}/_{α}\}}

[com_{2}]  \frac{S \overline{}^{(β)@α} S′ T \overline{}^{α?γ} T′}{S|T \overline{}^{τ} (β)(S′|T′\{^{β}/_{α}\})} if β ∉ fn(T)
[spawn] \frac{P ≻ α!Q.P′}{(β, P) \overline{}^{τ} (β, P′)|(α, Q)}
[internal] \frac{P ≻ τ.P′}{(α, P) \overline{}^{τ} (α, P′)}

[par]  \frac{S \overline{}^{m} S′}{S|T \overline{}^{m} S′|T} if bn(m) ∩ fn(T) = ∅

[res]  \frac{S \overline{}^{m} S′}{(α)S \overline{}^{m} (α)S′} if α ∉ fn(m)

[struct] \frac{S ≡ S′ S′ \overline{}^{m} T′ T′ ≡ T}{S \overline{}^{m} T}

Table 1: The labelled transition semantics of Plain LAL

m ::= τ | α?β | α@β | (α)@β

The first two indicate internal and input actions respectively, the third means that the agent contains the free name α at the free name β and the last means that the agent contains the bound name α at the free name β. The transition relation \overline{}⊆ (Agent×Label×Agent) is the smallest relation satisfying the rules in Table 1.

3 Bisimulations

For value passing calculi several formulations of bisimulations have been proposed, among these early, late and open bisimulation. In this section we shall define these for Plain LAL and study their relationship.

Though quite similar in definition they all differ in the case of the πcalculus. The main result of this article is that these in fact coincide in the case of Plain LAL.

The notion of early bisimulation was first defined in [MPW89]; the idea is that a transition can be matched in different ways, depending on the value that is being communicated. In our setting we have:

Definition 1 Early bisimulation A relation R is an early bisimulation if it is symmetric and S R T implies

• If S \overline{}^{α?γ} S′ then for every name β ∈ Name there exists a T′ such

that T \overline{}^{α?γ} T′ and S′\{^{β}/_{γ}\} R T′\{^{β}/_{γ}\}.

• If S \overline{}^{m} S′ and m ∈ \{τ, β@α, (β)@α\} then there exists a T′ s.t.

T \overline{}^{m} T′ and S′ R T′.

Two programs S and T are early bisimilar, written S ∼ T, if S R T for some early bisimulation R.

Late bisimulation was also defined in [MPW89]. Intuitively, the difference is that a transition must be matched by the same move, irrespective of the value communicated. In Plain LAL, we get:

Definition 2 (Late bisimulation) A relation R is a late bisimulation if it is symmetric and S R T implies

• If S \overline{}^{α?γ} S′ then there exists a T′ such that T \overline{}^{α?γ} T′ and for every name β S′{^{β}/_{γ}} R T′{^{β}/_{γ}}.

• If S \overline{}^{m} S′ and m ∈ \{τ, β@α, (β)@α\} then there exists a T′ s.t.

T \overline{}^{m} T′ and S′ R T′.

Two programs S and T are late bisimilar, written S ∼_{L} T, if S R T for some late bisimulation R.

Finally, open bisimulation, a notion of equivalence first studied by [San93]. The underlying idea is that one should consider matches for all possible instantiations of variables.

Definition 3 (Open bisimulation) A relation R is an open bisimulation if it is symmetric and S R T implies that for all substitutions ϑ ∈ Name → Name it holds that if Sϑ \overline{}^{m} S′ then there exists a T′ such that T ϑ \overline{}^{m} T′ and S′ R T′.

Two programs S and T are open bisimilar, written S ∼_{O} T, if S R T for some open bisimulation R.

By inspecting the definitions, it is easy to see that ∼_{O}⊆∼_{L}⊆∼. Further, it is relatively easy to verify that all three are indeed equivalence relations and also that they are congruence relations with respect to all operators but prefixing. In fact they are also congruences with respect to prefixing; we shall return to this later.

To prove our results in the following we shall exploit the techniques of up-to bisimulations. It is quite simple to prove that this principle is also sound for Plain LAL.

We shall now investigate how these 3 definitions of bisimulation relate to each other. But first we need the following lemma which states an important difference between synchronous and asynchronous communication

Lemma 1 S has a τ-transition, S \overline{}^{τ} T, due to an internal communication on a free name α iff either

• S \overline{}^{β@α} S′ \overline{}^{α?γ} S′′ with T ≡ S′′\{^{β}/_{γ}\}

• S \overline{}^{(β)@α} S′ \overline{}^{α?γ} S′′ with T ≡ (β)S′′\{^{β}/_{γ}\}

Proof. We have either S ≡ S′|(α, β) or S ≡ (β)(S′|(α, β)). □

Observe that the if part of the above lemma does not hold in a synchronous calculus because in a synchronous calculus a sequential process cannot communicate with itself. For instance we have ᾱβ.α(γ) \overline{}^{ᾱβ} α(γ) \overline{}^{α(γ)} 0 in the π-calculus but clearly we cannot have internal communication on α.

Using Lemma 1 we can now state the following theorem which turns out to be extremely important.

Theorem 2 If S ∼ T then S{^{α}/_{γ}} ∼ T {^{α}/_{γ}} for all α ∈ Name.

Proof. We show that R = {(S{^{α}/_{γ}}, T {^{α}/_{γ}}) | S ∼ T } is an early bisimulation up to structural congruence.

The proof proceeds by inspecting the possible transitions from S{^{α}/_{γ}}. We only consider two cases:

S\{^{α}/_{γ}\} \overline{}^{β?δ} S′′: Then either S \overline{}^{β?δ} or S \overline{}^{γ?δ} with β = α.

For S \overline{}^{β?δ} S′ we have S′′ = S′\{^{α}/_{γ}\}. Since S ∼ T we have for all η ∈ Name that T \overline{}^{β?δ} T′ such that S′\{^{η}/_{δ}\} ∼ T′\{^{η}/_{δ}\}. Further we must have T \{^{α}/_{γ}\} \overline{}^{β?δ} T′\{^{α}/_{γ}\} since γ ≠ β. Now for all η we have S′{^{α}/_{γ}}{^{η}/_{δ}} R T′{^{α}/_{γ}}{^{η}/_{δ}} where we w.l.o.g. assume that δ ≠ α, δ ≠ γ and η ≠ γ.

For S \overline{}^{γ?δ} S′ we have S′′ = S′\{^{α}/_{γ}\}. Since S ∼ T we have for all η ∈ Name that T \overline{}^{γ?δ} T′ such that S′\{^{η}/_{δ}\} ∼ T′\{^{η}/_{δ}\}. Hence

T \{^{α}/_{γ}\} \overline{}^{α?δ} T′\{^{α}/_{γ}\} is a matching move.

S\{^{α}/_{γ}\} \overline{}^{τ} V: Then either S \overline{}^{τ} S′ with V = S′\{^{α}/_{γ}\} in which case the proof is similar to the above, or the transition is due to internal communication on α. We examine the latter case.

Since α is free we have by Lemma 1 one of two:

i. S\{^{α}/_{γ}\} \overline{}^{β@α} V′ \overline{}^{α?δ} V′′ and V ≡ V′′\{^{α}/_{δ}\}.

ii. S\{^{α}/_{γ}\} \overline{}^{(β)@α} V′ \overline{}^{α?δ} V′′ and V ≡ (β)V′′\{^{β}/_{δ}\}.

We shall only consider case ii. Assume w.l.o.g. that β ≠ γ, δ ≠ γ and α ≠ δ. It is fairly obvious that either S \overline{}^{(β)@α} S′ \overline{}^{γ?δ} S′′ or

S \overline{}^{(β)@γ} S′ \overline{}^{α?δ} S′′ with S′\{^{α}/_{γ}\} = V′ and S′′\{^{α}/_{γ}\} = V′′ since S

could not do the transition. We assume w.l.o.g. that it is the second

case. Then T \overline{}^{(β)@γ} T′ \overline{}^{α?δ} T′′ with S′ ∼ T′ and S′′\{^{β}/_{δ}\} ∼ T′′\{^{β}/_{δ}\}.

Further we must have T \{^{α}/_{γ}\} \overline{}^{(β)@α} T′\{^{α}/_{γ}\} \overline{}^{α?δ} T′′\{^{α}/_{γ}\} and hence

by Lemma 1 T \{^{α}/_{γ}\} \overline{}^{τ} (β)T′′\{^{α}/_{γ}\}\{^{β}/_{δ}\}^{1}. Now we have

V ≡ (β)S′′{^{α}/_{γ}}{^{β}/_{δ}} = ((β)S′′{^{β}/_{δ}}){^{α}/_{γ}} R (β)T′′{^{α}/_{γ}}{^{β}/_{δ}}

A symmetric argument exists for T \{^{α}/_{γ}\} \overline{}^{m} V. □

As an immediate corollary we have that all our definitions of bisimulation coincide.

Corollary 3 Early, late and open bisimilarity coincide.

1This does not hold in the π-calculus.

Proof. Early bisimilarity implies open because by Theorem 2 we know that if S ∼ T then for every substitution ϑ we have Sϑ ∼ T ϑ. Therefore we can drop the substitution in the input case of the definition of early bisimulation. We now have that for every transition Sϑ \overline{}^{m} S′ there exists a T′ such that T ϑ \overline{}^{m} T′ with S′ ∼ T′, hence ∼ is an open bisimulation. □

This result is really interesting, as in the π-calculus, even without the match operator, early bisimulation is strictly coarser than late bisimulation which in turn is strictly coarser than open bisimulation. This is evidence that the expressive power of asynchronous communication is in fact less than that of synchronous communication.

A more pragmatic consequence of Corollary 3 is that it does not matter which definition of bisimilarity we use because we know that the underlying equivalence is the same.

Corollary 4 (Congruence) ∼ is a congruence relation.

Proof. Since ∼ is an open bisimulation it is clear that ∼ must be a congruence with respect to prefixing. □

The result above does not hold for the π-calculus where neither early nor late bisimulation is a congruence.

As stated in the proof of Corollary 3 we have by Theorem 2 that if we omit the substitution in the input case of the definition of early bisimulation we do not get a coarser relation. However, the definition we end up with is the definition of ground bisimulation. Thus we have no less than 6 bisimulations which are different in the π-calculus and coincide in Plain LAL. Despite this, by closer inspection it turns out that the only essential limitation Plain LAL has to the π-calculus is a more limited type of summation, since it can be shown that all π-calculus operators except the general operator can be encoded in plain LAL ([HK94]).

3.1 Weak Bisimulation

The proofs in the proof above are not dependent on dealing with strong bisimulations and are easily generalized to weak bisimulation. Hence all weak versions of the above bisimulations (save early and late congruence) are equal to the weak bisimulation given by the following definition. We define a weak transition as Definition 4 The relation ⟹ ⊆ (Agent × Label ∪ {ε} × Agent) is given by:

[figure: ⟹^{m}; =; τ; ∗; m; ⟹^{ε}; =; τ; ∗]

Definition 5 (Weak bisimulation) A relation R is a weak bisimulation if it is symmetric and S R T implies If S \overline{}^{m} S′ then there exists a T′ s.t. T ⟹^{m̂} T′ and S′ R T′ where τ̂ = ϵ and m̂ = m for m ≠ τ. Two programs S and T are weak bisimilar, written S ˙≈ T, if S R T for some weak bisimulation R.

4 Equational Theories for Finite Plain LAL

In the rest of the paper we shall present sound and complete axiomatizations of strong and weak bisimulation for finite Plain LAL, i.e. Plain LAL without replication. The usual way of proving completeness is by means of a normal form to which all bisimilar agents can be converted. This is not immediately possible in LAL as sum and parallel composition operate on two different levels. To deal with this, we extend the syntax of programs with prefixing and sum:

S ::= ∑_{i∈I} m_{i}.S_{i} | ⋯ where m ::= τ | α?β

Observe that we do not have spawn prefixes at this level as these are seen as τ-actions from the outside and can be modelled as such. Since the set of prefixes at system level is a subset of the set of labels we use the same letters as metavariables. With the extended syntax we get both sum and composition at system level and this enables us to define expansion theorems. We define the semantics of this new construct by extending the transition relation \overline{}with the following rule:

∑_{i∈I} m_{i}.S_{i} \overline{}^{m_{j}} S_{j} if j ∈ I

and we define ∑_{∅} S = •.

4.1 Axiomatization of Strong Bisimulation

In this section we shall give a complete axiomatization of ∼ for Plain LAL agents of the extended syntax.

We shall need to decide whether a restricted name can become accessible from outside, such that it can be used to get a value. Intuitively, a name can become accessible if it is located at an unrestricted location. With this definition α can become accessible in (α)((β, α)|(α, γ)) but not in (α)(σ) ((β, σ)|(σ, α)|(α, γ)). But in the last expression α can clearly become accessible through β and σ — we therefore need to be able to follow a sequence of names and to this end we define a notion of reachability:

Definition 6 (Reachability) Let S = (L) ∏(α_{i}, β_{i}). We say α_{j} is reachable in S if either α_{j} is free or there exists a sequence γ_{1}, …, γ_{n} where for 1 ≤ i < n we have for some k: γ_{i} = α_{k} and γ_{i+1} = β_{k}, further γ_{1} is free and γ_{n} = α_{j}. If α is not reachable in S we say that α is unreachable in S.

Observe that if α is not a location of a value we consider it unreachable. Further observe that reachability of a name is a strictly syntactic predicate, thus it is always decidable.

The axioms are given in Table 2

We shall denote by A this set of rules and axioms, and we write A ⊢ S = T if S = T can be proven using equational reasoning over the rules of A.

4.2 Soundness and Completeness

Theorem 5 (Soundness) If A ⊢ S = T then S ∼ T

Proof. We just need to show that the axioms hold if we replace = by ∼. □

Completeness is established through the concept of head normal forms and the notion of depth of an agent. The depth of an agent is the maximal length of any transition sequence that the agent can perform (a precise definition can be found in [HK94].)

Definition 7 (Head normal form) S is on head normal form, abbreviated hnf., if

S = (L) (∑ m_{i}.S_{i} | ∏ (α_{j}, β_{j}))

where L ⊆ ⋃{β_{j}}, L\ ⋃{β_{j}} ∩ fn(m_{i}) = ∅ and for all k in the index set is α_{k} reachable in (L) ∏(α_{j}, β_{j}).

C1 S = T if S ≡ T
C2 α?β.S = α?β.T if S = T
C3 τ.S = τ.T if S = T
C4 (α)S = (α)T if S = T
C5 S_{1}|S_{2} = T_{1}|T_{2} if S_{1} = T_{1} and S_{2} = T_{2}
C6 ∑_{I} m_{i}.S_{i} = ∑_{I} n_{i}.T_{i} if ∀j ∈ I : m_{j}.S_{j} = n_{j}.T_{j}
S1 (α, ∑ a_{i}.P_{i}) = ∑ m_{i}.S_{i} where \{ \begin{matrix}m_{i} = a_{i}, S_{i} = (α, P_{i}) & if a_{i} = τ, β?γ \\ m_{i} = τ, S_{i} = (α, P_{i})|(β, Q) & if a_{i} = β!Q \end{matrix}
S2 ∑_{I} S_{i} = ∑_{I\{k}} S_{i} if S_{j} = S_{k} for some j ∈ I\{k}
S3 (α) ∑ m_{i}.S_{i} = ∑ m_{i}.(α)S_{i} if α ∉ ⋃ n(m_{i})
S4 (α) ∑ m_{i}.S_{i} = (α) ∑_{m_{i}≠α?β} m_{i}.S_{i}

E1 S|T = ∑ m_{i}.(S_{i}|T) + ∑ n_{j}.(S|T_{j})

if S = ∑ m_{i}.S_{i}, T = ∑ n_{j}.T_{j} and bn(m_{i}) ∩ fn(T) = ∅ = bn(n_{j}) ∩ fn(S)

E2 (L) (∑ m_{i}.S_{i} | (α, β)| ∏(α_{j}, β_{j})) = (L) ( ∑_{m_{i}≠α?γ} m_{i}. (S_{i}|(α, β))

+ ∑_{m_{i}=α?γ} τ.S_{i}{β/γ} | ∏(α_{j}, β_{j}))
if α is unreachable in (L) ∏(α_{j}, β_{j})

Table 2: The equational theory for strong bisimilarity Lemma 6 If S if a finite Plain LAL process then there exists a hnf. H of no greater depth s.t. A ⊢ S = H.

Proof. Induction in the structure of S. □

We can now prove completeness:

Theorem 7 (Completeness) Let S and T be finite Plain LAL terms. If S ∼ T then A ⊢ S = T

Proof. We have S ∼ T. The proof is by induction in the maximal depth of S and T. □

4.3 Axiomatization of Weak Bisimulation

It is well-known that weak bisimulation is not a congruence, not even if we close it under substitutions, as it is not preserved by summation. For that reason we shall introduce another bisimulation similar to Milner’s observation equality.

Definition 8 Two agents S and T are observation equivalent, written S ≍ T if

• Whenever S \overline{}^{m} S′ then there exists a T′ s.t. T ⟹^{m} T′ and S′ ˙≈ T′.

and vice versa.

Observe that if the first move is a τ transition it cannot be matched by an εtransition. However, after the first move we only require weak bisimulation to hold. It can be shown that ≍ is the induced congruence of ˙≈.

Observation equivalence is related to weak bisimulation as stated by the following proposition:

Proposition 8 S ˙≈ T iff S ≍ T, S ≍ τ.T or τ.S ≍ T.

Proof. As in [Mil89] □

Normally, when defining normal forms for completeness proofs one eliminates parallel composition. In the previous section we saw that we could allow a limited use of parallel composition and still be able to prove completeness in the case of strong bisimulation. We have not been able to accomplish this for weak bisimulation. To get around this we extend the prefixes of agents to incorporate all labels of the labelled transition system; this does not require any changes in the semantics.

The axiom system AA consists of the axioms C1, C3 − C6 and S1 − S2 from the axiom system A and the following six:

C2 α?γ.S = α?γ.T if S{β/γ} = T {β/γ} for all β ∈ fn(S|T) ∪ {γ}
E1 (α, β) = β@α.0
E2 S|T = ∑ m_{i}.(S_{i}|T) + ∑ n_{j}.(S|T_{j})+

∑_{\begin{matrix}m_{i} = α?γ \\ n_{j} = β@α \end{matrix}}τ.(S_{i}\{β/γ\}|T_{j}) + ∑_{\begin{matrix}m_{i} = β@α \\ n_{j} = α?γ \end{matrix}}τ.(S_{i}|T_{j}\{β/γ\})

if S = ∑ m_{i}.S_{i}, T = ∑ n_{j}.T_{j} and bn(m_{i}) ∩ fn(T) = ∅ = bn(n_{j}) ∩ fn(S)

S3 (β) ∑ m_{i}.S_{i} = ∑_{β∉fn(m_{i})} m_{i}.(β)S_{i} + ∑_{\begin{matrix}m_{i} = β@α_{i} \\ β ≠ α_{i} \end{matrix}}(β)@α_{i}.S_{i}

T 1 S + τ.S = S if S is a summation
T 2 m.τ.S = m.S

The axioms T 1 and T 2 are similar to the well-known τ-laws of CCS; the third CCS τ-law is concerned with τ-transitions after a visible action and is thus not relevant in our case. The axiom C2 is necessary because in the extended syntax we no longer have preservation of bisimulation under substitution, as we now end up with a synchronous calculus. Alternatively we could have limited the set of processes to processes which are bisimilar to processes of Plain LAL.

Theorem 9 If AA ⊢ S = T then S ≍ T

Proof. The axioms hold then replacing = by ≍, and the rules preserve soundness. □

To prove completeness we introduce standard forms:

Definition 9 S is in standard form if

S = ∑ m_{i}.S_{i}

and the S_{i}’s are in standard form.

Lemma 10 For every finite agent S there there exists a standard form T of no greater depth s.t. AA ⊢ S = T.

Proof. The proof goes by induction in the structure of S. □

As is usual, we need to refine the notion of standard form to full standard form:

Definition 10 A standard form S is a full standard form if S ⟹^{m} S′ im-

plies S \overline{}^{m} S′.

Lemma 11 For every finite agent S there there exists a full standard form T of no greater depth s.t. AA ⊢ S = T.

We now get

Theorem 12 (Completeness) If S ≍ T then AA ⊢ S = T.

Proof. By Lemma 11 we can assume that S and T are full standard forms. The proof proceeds by induction in the depths of S and T. □

We have now shown how to axiomatize ≍, though it was ˙≈ we really wanted to axiomatize. However, by Proposition 8 we have S ˙≈ T iff either AA ⊢ S = T, AA ⊢ S = τ.T or AA ⊢ τ.S = T.

It is obvious that two processes can effectively be put in standard form. Furthermore by inspection of the proof of Theorem 7 and Theorem 12 we see that it can effectively be checked whether two processes in standard form are bisimilar and weak bisimilar respectively. It now follows that S ∼ T is decidable, furthermore S ≍ T is decidable and hence S ˙≈ T is decidable.

Observe that we need to extend the calculus not because it is asynchronous but because it is two-level. Compared to the axiomatization of the π-calculus in [PS93] we see that we end up with almost the same axioms. The main difference being that we have a simpler rule for input prexing in the strong case.

5 Conclusions and Related Work

In this paper we have put forward an asynchronous process calculus, Plain LAL, and defined the notions of early, late and open bisimulation equivalence within the setting of the operational semantics provided. It turns out that these notions of bisimulation coincide here. We give a sound and complete axiomatization of the common notion of bisimulation equivalence for finite Plain LAL agents.

Plain LAL looks somewhat different from the calcui of [HT91] and [Bou92] but it is in fact quite easy to come up with compositional encodings of these calculi in Plain LAL. Although we have not persued this subject very further, this leeds us to belive that our results will indeed also hold for asynchronous versions of the π-calculus.

An interesting question is: How much can we extend Plain LAL before the three definitions of bisimulation differ? For instance, if we introduce the matching operator of the π-calculus, the two agents (α, τ.β! + τ) and (α, τ.β! + τ + τ.[β = γ]β!) are late bisimilar but not open.

The ideas from Plain LAL can be extended to a higher-order calculus which allows the passing of processes. This calculus, called LAL, is similar to CHOCS ([Tho90]) and has been studied in [HK94]. It turns out that Corollary 3 also holds for LAL. Further, there is an adequate translation of LAL into Plain LAL – thus, the equational theory for Plain LAL can be used in conjunction with the translation to provide equational reasoning for LAL agents.

One should also note an important difference between our calculus and the fork calculus studied by [Hav94] which seems to indicate that an implicit parallel operator works better in the setting of asynchrony. For in the setting of the fork calculus the formulation of the bisimulation congruence becomes quite difficult, whereas the bisimulation congruence of Plain LALis entirely straightforward, being the bisimulation equivalence itself.

References

[BMT92] D. Berry, R. Milner, and D.N. Turner. A semantics for ml concurrency primitives. Conference Record of the 19th Annual ACM Symposium on Principles of Programming Languages, January 1992.

[BN92] Michele Boreale and Rocco De Nicola. Testing equivalences for mobile processes. In W.R. Cleaveland, editor, CONCUR ’92, number 630 in Springer LNCS, pages 2–16. Springer-Verlag, 1992.

[Bou92] Gérard Boudol. Asynchrony and the π-calculus. Technical report, INRIA Sophia-Antipolis, 1992.

[GB82] David Gelernter and Arthur J. Bernstein. Distributed communication via global buffer. In Proceedings of ACM Symposium on Principles of Distributed Computing, pages 10–18, August 1982.

[Hav94] Klaus Havelund. The Fork Calculus. PhD thesis, Department of Computer Science, University of Copenhagen, January 1994.

[HK94] Martin Hansen and Josva Kleist. Process calculi with asynchronous communication. Master’s thesis, Aalborg University, 1994.

[HT91] K. Honda and M. Tokoro. An object calculus for asynchronous communication. In ECOOP 91, volume 512 of Lecture Notes in Computer Science, pages 133–147. Springer-Verlag, 1991.

[HY93] Kohei Honda and Nobuko Yoshida. On reduction-based process semantics. In Proceedings of FST & TCS, volume 761 of Lecture Notes in Computer Science, pages 373–387. Springer, 1993.

[Ing94] Anna Ingólfsdóttir. Late and early semantics coincide for testing. Theoretical Computer Science, 1994. To appear.

[Mil89] Robin Milner. Communication and Concurrency. Prentice Hall, 1989.

[MPW89] Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes — part i and ii. Technical Report ECS-LFCS-89-85 and -86, Department of Computer Science, University of Edinburgh, 1989. Also published in Information and Computation, 100:1-77,1992.

[Ode95] Martin Odersky. Applying π: Towards a basis for concurrent imperative programming. In U.S. Reddy, editor, Proceedings of Second ACM SIGPLAN Workshop on State in Programming Languages (SIPL’95), pages 95–108. Dept. of Computer Science, Univ. of Illinois, January 1995. Technical Report no. UIUCDCS-R-95-1900.

[PS93] Joachim Parrow and Davide Sangiorgi. Algebraic theories for name-passing calculi. Information and Computation, 1993. To appear. Also available as Report ECS-LFCS-93-262, Department of Computer Science, University of Edinburgh, 1993.

[San93] Davide Sangiorgi. A theory of bisimulation for the π-calculus. In E. Best, editor, Proceedings of CONCUR 93, volume 715 of Lecture Notes in Computer Science, pages 127–142. Springer-Verlag, 1993.

[Tho90] Bent Thomsen. Calculi for Higher-Order Communicating Systems. PhD thesis, Imperial College, University of London, 1990.

Recent Publications in the BRICS Report Series

RS-96-8 Martin Hansen, Hans H� uttel, and Josva Kleist. Bisimulations for Asynchronous Mobile Processes. April 1996. 18 pp. Appears in Tbilisi Symposium on Language, Logic, and Computation, 1995.

RS-96-7 Ivan Damg� ard and Ronald Cramer. Linear Zero-Knowledegde - A Note on Ef�cient Zero-Knowledge Proofs and Arguments. April 1996. 17 pp.

RS-96-6 Mayer Goldberg. An Adequate Left-Associated Binary Numeral System in the λ-Calculus (Revised Version). March 1996. 19 pp. Accepted for Information Processing Letters. This report is a revision of the BRICS Report RS-95-38.

RS-96-5 Mayer Goldberg. G� odelisation in the λ-Calculus (Extended Version). March 1996. 10 pp.

RS-96-4 J�rgen H. Andersen, Ed Harcourt, and K. V. S. Prasad. A Machine Veri�ed Distributed Sorting Algorithm. February 1996. 21 pp. Abstract appeared in 7th Nordic Workshop on Programming Theory, NWPT ’7 Proceedings, 1995.

RS-96-3 Jaap van Oosten. The Modi�ed Realizability Topos. February 1996. 17 pp.

RS-96-2 Allan Cheng and Mogens Nielsen. Open Maps, Behavioural Equivalences, and Congruences. January 1996. 25 pp. A short version of this paper is to appear in the proceedings of CAAP ’96.

RS-96-1 Gerth St�lting Brodal and Thore Husfeldt. A Communication Complexity Proof that Symmetric Functions have Logarithmic Depth. January 1996. 3 pp.

RS-95-60 J�rgen H. Andersen, Carsten H. Kristensen, and Arne Skou. Speci�cation and Automated Veri�cation of Real-Time Behaviour � A Case Study. December 1995. 24 pp. Appears in 3rd IFAC/IFIP workshop on Algoritms and Architectures for Real-Time Control, AARTC ’95 Proceedings, 1995, pages 613�628.