Algebra of Broadcasting Systems: Value Passing, Sequential Composition, and Fork

Martin Weichert^{∗}^{†}

December 5, 1994

Abstract

This paper presents ACBS&, Algebra of Broadcasting Systems with Fork, a process calculus with broadcast communication, which combines value passing and sequential composition.

Putting value passing into a calculus with sequential composition turns out to be more complicated than with a prefixing calculus. A semantics for such a calculus can be defined using environments, as in imperative languages.

Parallel processes have parallel environments, which can lead to ambiguity which of the environments shall be passed on to the sequentially following process. ACBS& solves this problem by distinguishing a foreground and a background process. The resulting operator can be interpreted as a fork operator, which “forks off” a background process.

The calculus is presented both in a “pure” and a value passing version, together with a complete axiomatisation for the pure calculus.

1 Introduction

The basic ingredients of the calculus ACBS& are:

• CBS with its basic idea broadcast communication, as presented in [Pra91, Pra92],

• first the “pure” and then the value passing version,

into which I have incorporated two ideas from the Dutch work on process algebra, like ACP as presented in [BW90]:

• sequential composition, as opposed to prefixing; with the consequence of having two different actionless processes o and 1, and

• parallel composition is split up into the three operators full merge, left merge, and communication merge; which facilitates axiomatisation.

Parallel composition, which is still present in the equational reasoning, has in the calculus itself been replaced by a fork operator, which “forks off” a background process.

∗Author’s address: Department of Computer Sciences, Chalmers University of Technology, S-412 96 Gothenburg, Sweden. E-mail: martinw@cs.chalmers.se

†This work was supported by the Esprit Basic Research Action CONCUR2

1.1 What is broadcasting?

In broadcasting communication as presented in [Pra91, Pra92], sending is autonomous and receiving is controlled. Any participant that is ready to speak can do so, while the listener(s) (of which there may be zero, one or many) have to wait until they hear something. The symmetric synchronisation of the handshake model is replaced by an asymmetric synchronisation: the listener is dependent on the speaker, but not the other way round.

The broadcasting model is based on local area networks as well as human speech, and gives rise to a number of interesting programming examples [Pra93].

1.2 Why prefer sequential composition over prefixing?

It is natural to think of events happening sequentially in time. You can express the notion of “repeating a process several times”, or even “forever”. Furthermore, it emphasizes the role of simple one-action-processes as the building blocks of bigger ones, thus enabling bottom-up process construction.

ACP and related calculi with sequential composition offer several models and axiom systems which are complete for those models. The left merge operator can helpturning an infinite axiom system into a finite one. But their communication primitive seems is predominantly handshake, due to the strong influence of CCS. Applying the ideas of ACP to broadcasting communication instead of handshaking has not been studied yet to my knowledge. This is the purpose of introducing ACBS.

The reader is assumed to be familiar with CCS-like calculi.

2 Discussion of the language constructs

The language presented here consists of a few, simple constructions. Several extensions with more operators and other concepts are possible - some of them face exactly the same problems as existing calculi, others pose quite unexpected new questions. A few of those will be discussed in section 5.

2.1 Simple Actions

The building blocks of processes are simple actions. There are two kinds of actions: send a! and receive a?, where a is the actual signal being transmitted. Their meaning is the same as in CBS.

Unlike CBS, an action here is itself a process: The process a! broadcasts the signal a into the environment, and then it terminates. It will ignore any incoming signals, and it does not depend on any other process(es) being ready to receive the signal. Sending is autonomous. The process a? waits until it hears the signal a being broadcast, and then terminates. It cannot ignore a when it comes, but it will ignore anything else. Receiving is dependent on sending.

With value passing, the process x?, which can receive any value (represented by the variable x), is different from the process a?, receiving a particular signal a.

The special signal τ represents noise, a “signal” that carries no information. It is different from the other signals in that it cannot be received.

2.2 Choice

P + Q can behave either as P, or as Q. Eg, the process a! +b? can either send an a or receive a b sent from some other process.

2.3 Empty processes

In contrast to prefix-based calculi like CCS and CBS, the use of sequential composition gives rise to two empty processes:

2.3.1 Termination

1 does no action, but terminates successfully. For any process P, 1 · P is the same as P. It is called ε in [BW90].

2.3.2 Inaction

o does nothing at all, and prevents anything else from happening afterwards. For any process P, o · P is the same as o. Is called δ or deadlock in [BW90].

2.4 Sequential Composition

P · Q stands for “first P, then Q”. If and when P has successfully terminated, Q can happen – like “;” in imperative programming languages.

Note that the condition “P has terminated” is not the same “P can do no more actions”. The latter is also true if P just aborts or deadlocks, in which case Q will never start.

In connection with the concept of “forking” processes, the meaning of “termination” itself changes: Process P in P · Q may have started some background process which is still alive when Q is allowed to start executing. Q will then run in parallel with what remains of process P. Instead of “termination” one should better talk about “passing control” from P to Q.

2.5 Parallel Composition. Fork

P ∥Q represents the two processes P and Q running in parallel. They can communicate via broadcast. Any of several processes in parallel that is ready to speak can do so, autonomously, while those processes that are ready to listen hear the message, and all others ignore it. P ∥Q terminates if and when both P and Q have terminated.

This calculus uses a variant of parallel, the fork operator.

P &Q is the process which first forks off process P, and then starts Q, from where on they both run in parallel, possibly communicating with each other. P &Q behaves exactly as P ∥Q, except for the passing of control to a process R sequentially composed after it: Whereas in (P ∥Q) · R both P and Q have to terminate to let R start, in (P &Q) · R the process R waits only for termination of Q. The latter expression is equivalent to P &(Q · R).

The symbol & is chosen because of its use in Unix shell scripts, where it has the same meaning. It can be defined either as a unary or a binary operator. Both of them are interdefinable in the presence of the other operators of this calculus: P & can be defined as P &1, and P &Q as (P &) · Q.

3 Pure ACBS&: The Syntax and Operational Semantics

3.1 Syntax

Process expressions in “pure” ACBS&, ie without value passing, are built using the following syntax:

Act : : = a? | a! | τ!
P : : = o | 1 | Act | P + P | P · P | P &P

The set of all process expressions is called P.

Let D be a set of data values used as “signals”, and D_{τ} = D ∪ {τ}. a, b range over signals, including τ where appropriate.

An action consists of a signal together with a punctuation symbol: a! “send a”, a? “receive a”, or a: “ignore a”. The latter is only part of the semantics, given below, it does not appear in the syntax. It is defined in such a way that “P ignores a” iff “P does not receive a”.

In the following, ♯ stands for !, ?, or :, ♮ stands for ! or ?, ♭ stands for ? or :.

3.2 Operational Semantics

The operational semantics of ACBS is given by a labelled transition relation on process expressions. There are two kinds of transitions:

P ⟶^{a♮} P′ is to be read as “process P does action a♮ and becomes P′”.

P ⟶^{√} P′ is to be read as “process P passes on control to the next process in sequential composition, with a “residual” process P′ remaining in the background.” There is an important special case where P′ is an inactive process,

like o. A transition like P ⟶^{√} o can be read simply as “P terminates”. The semantics is presented in Table 1.

4 Bisimulation and Axiomatisation

Our goal is to find a set of rules for equational reasoning about the calculus, which characterise the desired equivalence between processes, the bisimularity (bisimulation equivalence).

First we define bisimulation via the operational semantics, then we present a set of rules which are sound and complete w r t bisimulation.

Operator  Send  Receive  Ignore^{1}  Pass Control
1, Termination  1 ⟶^{√} o
o, Inaction  o ⟶^{a:}
?, Listen  a? ⟶^{a?} 1  a? ⟶^{b:} (if a ≠ b)
!, Send  a! ⟶^{a!} 1  a! ⟶^{b:}

{+, Choice \atop (i ∈ \{1, 2\})}  \frac{P_{i} ⟶^{a♮} P′}{P_{1} + P_{2} ⟶^{a♮} P′}  \frac{P_{1} ⟶^{a:} P_{2} ⟶^{a:}}{P_{1} + P_{2} ⟶^{a:}}  \frac{P_{i} ⟶^{√} P′}{P_{1} + P_{2} ⟶^{√} P′}

·, Sequential Composition

\frac{P ⟶^{a♯} P′}{P · Q ⟶^{a♯} P′ · Q}

”  \frac{P ⟶^{√} P′ P′&Q ⟶^{α} R}{P · Q ⟶^{α} R}

&, fork^{2}  \frac{P ⟶^{a♯_{1}} P′ Q ⟶^{a♯_{2}} Q′}{P &Q ⟶^{a(♯_{1}•♯_{2})} P′&Q′} (♯_{1} •♯_{2} ≠ ⊥) \begin{matrix}• & ! & ? & : \\ ! & ⊥ & ! & ! \\ ? & ! & ? & ? \\ : & ! & ? & : \end{matrix}

”  \frac{P ⟶^{√} P′ P′&Q ⟶^{a♮} R}{P &Q ⟶^{a♮} R} \frac{P ⟶^{√} P′ P′&Q ⟶^{a:}}{P &Q ⟶^{a:}}

”  \frac{Q ⟶^{√} Q′}{P &Q ⟶^{√} P &Q′}

1 P ⟶^{a:} is an abbreviation for P ⟶^{a:} P 2 ⊥ means “undefined” in the communication algebra (right) for •

Table 1: Transition rules for the “pure” calculus

4.1 Strong Bisimulation

(Bi)simulation is defined as usual.^{1}

Definition 1 [Simulation, Bisimulation] R ⊆ P × P is a simulation if R^{⊤} · →^{a♯} ⊆ →^{a♯} · R^{⊤} for all a♯. R is a bisimulation if both R and R^{⊤} are simulations.

As in CCS/CBS, the largest bisimulation^{2} is an equivalence, denoted by ∼.

Proposition 2 ∼ is a congruence.

4.2 Laws

The following laws make use of some auxiliary operators, which are not mentioned in the syntax given above. The purpose of these operators is not to build processes, they only appear in the reasoning about processes.

The process P &Q is identical to P ∥Q, except for their termination behavior: P &Q terminates if and when Q does. Termination of the “background process” P has no effect at all. Therefore we have the equality:

P &Q = (P · o)∥Q

The three operators full merge ∥, left merge ⌊⌊, and communication merge − ∥ are taken from ACP [BW90]. We use the symbol − ∥ for communication merge; in ACP it is written |.

P ∥Q has in general three possibilities for its first action: Either P can do an action (which Q ignores), or Q does an action (which P ignores), or both of them engage in a communication action between them. These three possibilities are reflected by the important equality:

P ∥Q = P ⌊⌊Q + Q⌊⌊P + P− ∥Q

P − ∥ Q must start with a communication action between P and Q. P ⌊⌊Q must start with an action from P, which Q ignores. If Q queries for a signal a, then it must listen to it when it comes - it cannot ignore it. Thus, the process P ⌊⌊Q cannot do an a-action if Q queries for a.

The actions of P ⌊⌊Q are therefore restricted by the “query set” of process Q, ie the set of all labels a such that Q can start with an a?-transition, written

as Q^{?} = {a: ∃Q′. Q ⟶^{a?} Q′}.

The restricted action a♮ \Q^{?} is the same as a♮ iff a is not in the set Q^{?}; otherwise it is equal to o.

The laws for strong bisimulation are given in Table 2.

1I prefer the concise formulation R^{⊤} · →^{a♯} ⊆ →^{a♯} · R^{⊤}, or, using the relational division operator, R^{⊤} ⊆ →^{a♯} · R^{⊤}/→^{a♯}, over the usual one, which is equivalent:

“whenever P RQ, if P ⟶^{a♯} P′ then ∃Q′ such that Q ⟶^{a♯} Q′ and P′RQ′ ”.

R^{⊤} is the converse (or “transpose”) of R.

2“Bisimulation” in this paper always means “strong”, unless explicitly stated that it is “weak”.

(+com)  P + Q = Q + P
(+ass)  (P + Q) + R = P + (Q + R)
(+idp)  P + P = P
(+o)  P + o = P
(o ·)  o · P = o
(1 ·)  1 · P = P
( · ass)  (P · Q) · R = P · (Q · R)
(+ ·)  (P_{1} + P_{2}) · Q = P_{1} · Q + P_{2} · Q
(but:  P · (Q_{1} + Q_{2}) ≠ P · Q_{1} + P · Q_{2} !)
(&∥)  P &Q = (P · o)∥Q
(exp)  P ∥Q = P ⌊⌊Q + Q⌊⌊P + P− ∥Q
(o⌊⌊)  o⌊⌊Q = o
(+⌊⌊)  (P_{1} + P_{2})⌊⌊Q = P_{1}⌊⌊Q + P_{2}⌊⌊Q
(♮⌊⌊)  a♮ ⌊⌊Q = a♮ \Q^{?} · Q
( · ⌊⌊)  (a♮ · P)⌊⌊Q = a♮ \Q^{?} · (P ∥Q)
(− ∥com)  P− ∥Q = Q− ∥P
(o− ∥)  o− ∥Q = o
(+− ∥)  (P_{1} + P_{2})− ∥Q = P_{1}− ∥Q + P_{2}− ∥Q
(♮− ∥)  a♮− ∥(b♮′ · Q) = (a♮− ∥b♮′) · Q
( ·− ∥) (a♮ · P)− ∥(b♮′ · Q) = (a♮− ∥b♮′) · (P ∥Q)
(!− ∥!)  a!− ∥a! = o
(!− ∥?)  a!− ∥a? = a!
(?− ∥?)  a?− ∥a? = a?
(− ∥≠)  a♮− ∥b♮′ = o, if a ≠ b
(\ ∈)  a♮ \Q^{?} = o, if a ∈ Q^{?}
(\ ∉)  a♮ \Q^{?} = a♮, if a ∉ Q^{?}
(o^{?})  o^{?} = ∅
(!^{?})  (a! )^{?} = ∅
(?^{?})  (a? )^{?} = {a}
(+^{?})  (P + Q)^{?} = P^{?} ∪ Q^{?}
( ·^{?})  (P · Q)^{?} = P^{?}

Table 2: Laws for strong bisimulation

Let

Laws = { (+com), (+ass), (+idp), (+o), (o ·), (1 ·), (+ ·), ( · ass), (&∥), (exp),
(o⌊⌊), (+⌊⌊), (♮⌊⌊), ( · ⌊⌊), (− ∥com), (o− ∥), (+− ∥), (♮− ∥), ( ·− ∥),
(!− ∥!), (!− ∥?), (?− ∥?), (− ∥≠), (\ ∈), (\ ∉), (o^{?}), (!^{?}), (?^{?}), (+^{?}), ( ·^{?}) }

Proposition 3 All of the laws are sound w r t ∼.

To prove eg that the law ( · ass) is sound w r t ∼, I show that the relation

R =^{def} {⟨(P · Q) · R, P · (Q · R)⟩: P, Q, R ∈ P} ∪ IdP

is a bisimulation.

(The relation

R′ =^{def} {⟨(P · Q) · R, P · (Q · R)⟩: P, Q, R ∈ P}

is not enough: For some P, Q and R, both (P · Q) · R and P · (Q · R) may have a transition to the same process, rather than to two processes which are in the relation R′.)

The soundness proofs can be machine checked. So far, I have translated the syntax and semantics of the calculus into the logical framework alf [MN94], and have proved the soundness of laws like 1 · P ∼ o&P and o&P ∼ P.

4.3 Basic Terms

A process expression is called a basic term if it is in the following form:

B = ∑_{i} a_{i}♮_{i} + ∑_{j} a_{j}♮_{j} · B_{j}

where the B_{j} themselves are basic terms. An empty sum stands for o.

4.4 Completeness

The above laws can be turned into a Term Rewriting System, by reading all the equal signs as arrows from left to right. That TRS reduces every process to a basic term:

Proposition 4 For every process P ∈ P, there is a basic term B ∈ P, such that

Laws ⊢ P = B

The proof works by induction over the structure of basic terms.

Basic terms that are bisimilar must have the same (ie, bisimilar) summands (modulo commutativity, associativity, and idempotence of + and occurrence of o).

Let

Laws^{+} = {(+com), (+ass), (+idp), (+o)}

Proposition 5 For all basic terms B_{1}, B_{2} ∈ P: if B_{1}∼B_{2} then

Laws^{+} ⊢ B_{1} = B_{2}

Thus,

Proposition 6 The set Laws is complete w r t bisimulation.

4.5 More laws

Some other interesting equalities, which are not needed for the completeness result, are stated below.

(∥o)  P ∥o = P · o
(∥com)  P ∥Q = Q∥P
(∥ass) (P ∥Q)∥R = P ∥(Q∥R)

4.6 Expansion Theorem

CCS-like calculi usually have an axiomatisation including an “Expansion Theorem”, which is really not an axiom but an axiom schema for infinitely many axioms. Note that the list above does not contain any explicit Expansion Theorem. Instead it has the equality (exp), which together with the distributivity laws for ⌊⌊ and − ∥ plays a similar role, thus making a finite axiomatisation possible. Faron Moller showed in his thesis [Mol89], that the ⌊⌊ operator is necessary for finite axiomatisation.

5 Extensions

5.1 Recursion

So far, all processes have finite transition trees. There are various ways the calculus can be extended to include some form of recursion and thus processes that have infinite transition trees.

The most general form of recursion allows a process to contain itself within any operator, eg

X = a! +b! · X · c!
Y = a! · (Y ∥b! )

Both processes X and Y have infinitely many different states in their transition trees.

If however recursion is restricted such that the recursive appearance of the process is not allowed within a parallel, and only on the right side of a sequential, then the process can only reach a finite number of different states.

The first form of recursion therefore appears to be more expressive. This difference in expressivity reminds of the one between context-free (Chomsky 2) and regular (Chomsky 3) languages.

5.1.1 Loop

A simple form of recursion is made possible by the sequential composition, P^{ω}, “repeat P forever”. It has the semantics rule:

\frac{P ⟶^{a♯} P′}{P^{ω} ⟶^{a♯} P′ · P^{ω}}

and the following laws:

(unfold) P^{ω} = P · P^{ω}
(fold) if X = P · X, then X = P^{ω}

5.1.2 Loop and Fork

Suppose we want to define a generator process Gen which, every time it receives a signal gen, creates a new copy of some process P to run in parallel with Gen itself. Gen can be written recursively as: Gen = gen? · (P ∥Gen). Using the (unary or binary) fork operator, this is equivalent to Gen = gen? · (P &Gen) or Gen = gen? · P & · Gen. Thus it can be rewritten with a loop as Gen = (gen? · P &)^{ω}. Thus, the loop operator as a “restricted” form of recursion is not so restricted after all. It is not clear whether this rewriting offers any advantage or only shifts the complexity to a different operator.

6 Discussion: Value Passing and Environments

6.1 Why environments? Prefixing vs. Sequential Composition

We extend the calculus with value passing.

Process expressions can be built with the following actions:

Act : : = τ! | e! | x?

where x stands for a variable, and e for any expression, possibly containing variables, yielding a result. The transition system defined in the operational semantics, however, is still labelled with single actions, not with variables or expressions.

In a prefixing calculus, processes can be defined as:

P : : = o | Act. P | P + P | P ∥P

Action x? binds the variable name x, which may occur free in e. In x! . P, x is free, in x? . x! . P it is bound.

With sequential composition, processes look like this:

P : : = o | Act | P · P | P + P | P ∥P

x? cannot be seen as a variable binding here, if we want · to be associative: The scope of x in (x? · P) · Q would be P, but in x? · (P · Q) it would be P · Q.

Now we want to give meaning to processes like x? · x!, by separately interpreting its parts x? and x! and combining them. In a prefixing calculus like CBS one can express value passing with a rule

x? . P ⟶^{v?} P [v/x]

(note that the two terms on both sides of the arrow have no free variables, though P itself does!). We have no directly corresponding rule here. If we try to define

x? ⟶^{v?} 1

we find that the information about the actually transmitted value v is lost. The prefixing calculus does not need to give any semantics to expressions with free variables, but we have to. By introducing environments, assignments of variable names to values, the information can be conveyed from one process to its successor. Receiving a value changes the environment:

⟨x? , ρ⟩ ⟶^{v?} ⟨1, ρ[v/x]⟩

Sending a value uses the information stored in the environment:

⟨e! , ρ⟩ ⟶^{([[e]]ρ)!} ⟨1, ρ⟩

The operational semantics is no longer a transition system between processes, but between processes augmented with environments:

→ ⊆ (P̄ × Env) × Act × (P̄ × Env)

Defining an operational semantics is more difficult, and also more imperativestyle. There is no value passing in ACP as presented in [BW90].

6.2 Environments of parallel processes

Each process running in parallel has its own environment, as given by the rule:

\frac{⟨P, ρ⟩ ⟶^{a♯_{1}} ⟨P′, ρ′⟩ ⟨Q, σ⟩ ⟶^{a♯_{2}} ⟨Q′, σ′⟩}{⟨P, ρ⟩∥⟨Q, σ⟩ ⟶^{a♯_{1}•♯_{2}} ⟨P′, ρ′⟩∥⟨Q′, σ′⟩}

This approach makes the variables local to each parallel component. It works fine for static systems, where the number of parallel processes stays constant all the time.

If we want to have dynamic systems, where processes can split into two, or join into one, we need some more rules.

6.3 Splitting processes

A process splits into two in the expression P · (Q∥R). Both Q and R start with the same environment that P ended up with. This will be made formal later, using augmented processes and configurations.

6.4 Joining processes

In (P ∥Q) · R, two processes join into one. When P and Q terminate with different environments ρ and σ, which environment should R inherit? (P and Q could for example perform two parts of a computation in parallel, the final result of which shall then be used by R.)

There are several possibilities.

6.4.1 Ranking

Out of several parallel components, one is declared as “main”, and its environment will be inherited.

6.4.2 Random

R inherits either ρ or σ by non-deterministic choice.

6.4.3 Combine

ρ and σ are somehow merged into one environment ρ ⊕ σ. A restriction on P and Q could be introduced that shared variables must be read-only.

6.4.4 Agree

P and Q both give a result; and the results given by both must agree. (cf Lotos).

6.4.5 Nothing

R gets no information out of P and Q. The scope of any variables occurring in P and Q is limited to these.

6.4.6 Disallow

Joining of processes if not allowed. The first operand of a sequential composition must not contain any ∥.

6.5 Fork

The problem with the joining processes is partly due to the symmetry of the parallel operator. In (P ∥Q) · R, R has to wait for both P and Q to terminate, and we don’t know from which of them R should inherit the environment. In contrast, in (P &Q) · R, R waits only for Q to terminate, so it seems natural to let R inherit the environment of Q.

7 ACBS& with Value Passing: The Syntax and Operational Semantics

After all these theoretic considerations, here is the calculus with value passing.

7.1 Syntax

ACBS& process expressions are built using the following syntax:

P : : = o | 1 | x? | e! | τ! | P + P | P · P | P &P

7.2 Operational Semantics

For the operational semantics with value passing we need some auxiliary definitions.

Processes are augmented with environments in certain positions.

The syntax for augmented processes is given by:

P̄ : : = o | 1 | x? | e! | τ! | P̄ + P̄ | P̄ · P | P̄, ρ&P̄

where P stands for a process, P̄ for an augmented process, and ρ for an environment. Note that the second component of a sequential composition is not augmented with an environment - it will inherit the one from its predecessor when that passes over control.

We will call a pair consisting of an augmented process and an environment, such as P̄, ρ (dropping the pairing parentheses), a configuration.

Augmenting a process P with an environment ρ is defined as follows:

\begin{aligned}oρ & = & o \\ 1ρ & = & 1 \\ x?ρ & = & x? \\ e!ρ & = & e! \\ (P_{1} + P_{2})ρ & = & P_{1}ρ + P_{2}ρ \\ (P · Q)ρ & = & P ρ · Q \\ (P &Q)ρ & = & P ρ, ρ&Qρ \end{aligned}

The operational semantics of ACBS with value passing is given by a labelled transition relation between configurations; so the semantics associated to a process P starting in an environment ρ will be the transition system of the configuration P ρ, ρ.

The semantics is presented in Table 3. P̃, P̃′, Q̃... range over configurations.

8 Denotational semantics. Implementation

The calculus can also be given a denotational semantics, where the process domain of transition trees is defined with the help of, eg, complete partial orders [Abr91] or metric spaces [vB93]. I have implemented the calculus (with value passing) in LML, a lazy functional language, by translating process terms into transition trees which I represent as lazy infinite data structures. In alf [MN94] I have done another implementation, so far only the “pure” calculus, and done some machine-assisted correctness proofs.

1, Termination  1, ρ ⟶^{√} o, ρ
o, Inaction  o, ρ ⟶^{v:}
?, Listen  x? , ρ ⟶^{v?} 1, ρ[v/x]  x? , ρ ⟶^{τ:}
!, Send  e! , ρ ⟶^{[[e]]ρ!} 1, ρ  e! , ρ ⟶^{v:}

{+, Choice \atop (i ∈ \{1, 2\})}  \begin{matrix}P_{i}, ρ & ⟶^{a♮} & P̃ & ′ \\ P_{1} + P_{2}, ρ & ⟶^{a♮} & P̃ & ′ \end{matrix}  \begin{matrix}P_{1}, ρ ⟶^{v:} & P_{2}, ρ ⟶^{v:} \\ P_{1} + P_{2}, ρ & ⟶^{v:} \end{matrix}  \begin{matrix}P_{i}, ρ & ⟶^{√} & P̃ & ′ \\ P_{1} + P_{2}, ρ & ⟶^{√} & P̃ & ′ \end{matrix}

·, Sequential Composition

\begin{matrix}P, ρ & ⟶^{a♯} & P′, ρ′ \\ P · Q, ρ & ⟶^{a♯} & P′ · Q, ρ′ \end{matrix}

”  \begin{matrix}P, ρ ⟶^{√} P̃′ & P̃′&Qρ, ρ ⟶^{α} R̃ \\ P · Q, ρ & ⟶^{α} & R̃ \end{matrix}

&, fork^{2}  \frac{P̃ ⟶^{a♯_{1}} P̃′ Q̃ ⟶^{a♯_{2}} Q̃′}{P̃&Q̃ ⟶^{a(♯_{1}•♯_{2})} P̃′&Q̃′} (♯_{1} •♯_{2} ≠ ⊥)  \begin{matrix}• & ! & ? & : \\ ! & ⊥ & ! & ! \\ ? & ! & ? & ? \\ : & ! & ? & : \end{matrix}

”  \frac{P̃ ⟶^{√} P̃′ P̃′&Q̃ ⟶^{a♮} R̃}{P̃&Q̃ ⟶^{a♮} R̃}  \frac{P̃ ⟶^{√} P̃′ P̃′&Q̃ ⟶^{v:}}{P̃&Q̃ ⟶^{v:}}

”  \frac{Q̃ ⟶^{√} Q̃′}{P̃&Q̃ ⟶^{√} P̃&Q̃′}

1 P, ρ ⟶^{v:} is an abbreviation for P, ρ ⟶^{v:} P, ρ

Table 3: Transition rules for the value passing calculus

2 ⊥ means “undefined” in the communication algebra (right) for •

9 Conclusions. Where to go on

9.1 Broadcast vs. Handshake

The work so far shows that broadcast communication can be realised in a sequential setting just as well as handshake communication. Nothing in ACP forces it to use handshaking. The difficulties encountered with value passing in a sequential setting are independent of the underlying communication model.

9.2 Sequential vs. Prefixing

The idea of sequential composition, a more “symmetric”, homogeneous operator than prefixing, seems appealing. As long as only the pure calculus is considered, sequential composition works just as well as prefixing. With value passing, however, things start getting difficult, without any obvious advantage of sequential composition to be seen.

The problem of passing values in some context with sequential and parallel composition is however quite a common one and appears in many different formalisms, such as Unix shell scripts, Lotos, “Fork Calculus” [Hav92], Concurrent ML, Occam, μCRL [Gro91]. The concept of forking seems promising towards a solution.

9.3 Other

A question not yet treated here is how to define a suitable weak bisimulation and which properties it will have. We are also looking for more motivating examples. Space didn’t permit me to put in here any of the examples I have, unfortunately.

10 Acknowledgements

Special thanks to my supervisor K.V.S. Prasad, without whom this work would not have been possible, to the concurrency group at Chalmers, and Thorsten Altenkirch for discussion and encouragement.

References

[Abr91] S. Abramsky. A domain equation for bisimulation. Information and Computation, 92(2):161–218, June 1991.

[BB93] J. C. M. Baeten and J. A. Bergstra. On sequential composition, action prefixes and process prefix. Technical Report P9305, University of Amsterdam, March 1993.

[BBK86] J. C. M. Baeten, J. A. Bergstra, and J. W. Klop. Decidability of bisimulation equivalence for processes generating context-free languages. Technical Report CS-R8632, Centre for Mathematics and Computer Science, Amsterdam, 1986.

[BW90] J. C. M. Baeten and W. P. Weijland. Process Algebra, volume 18 of Tracts in Theoretical Computer Science. Cambridge Univ. Press, 1990.

[CHM93] Søren Christensen, Yoram Hirshfeld, and Faron Moller. Bisimulation equivalence is decidable for all basic parallel processes. In CONCUR-93, Hildesheim, 1993.

[Gro91] Jan Friso Groote. Process Algebra and Structured Operational Semantics. PhD thesis, Universiteit van Amsterdam, November 1991.

[Hav92] Klaus Havelund. The fork calculus, 1992. presented at the Workshop in Bergen, fall 1992.

[HL92] Matthew Hennessy and Huimin Lin. Symbolic bisimulations. Computer Science Internal Report 1/92, University of Sussex, April 1992.

[Mil80] Robin Milner. A Calculus of Communicating Systems. Lecture Notes in Computer Science. Springer-Verlag, 1980.

[MN94] Lena Magnusson and Bengt Nordström. The ALF proof editor and its proof engine. In Types for Proofs and Programs, LNCS, pages 213–237, Nijmegen, 1994. Springer-Verlag.

[Mol89] Faron Moller. Axioms for Concurrency. PhD thesis, University of Edinburgh, October 1989.

[Pra91] K. V. S. Prasad. A calculus of broadcasting systems. In TAPSOFT’91 Volume 1: CAAP, April 1991. Springer Verlag LNCS 493.

[Pra92] K. V. S. Prasad. A calculus of value broadcasts. Technical Report 69, Department of Computer Science, Chalmers University of Technology, October 1992.

[Pra93] K. V. S. Prasad. Programming with broadcasts. Technical Report 74, Department of Computer Science, Chalmers University of Technology, September 1993.

[vB93] Franck van Breugel. Three metric domains of processes for bisimulation. Technical Report CS-R9335, CWI, Amsterdam, 1993.

[Wei93] Martin Weichert. Algebra of communicating systems. In Wintermötet Tanum Strand, January 1993. Draft Proceedings.

[Wei94] Martin Weichert. Value passing and sequential composition. In Proceedings of La Wintermöte ’94 Lundsbrunn, January 1994.