Spring 1996

G. Agha,

P.C. Kanellakis and S.A. Smolka, CCS Expressions, finite state processes, and three problems of equivalence, Information and Computation 86, 43--68, 1990.

R. Milner, Semantics of Concurrent Processes, in J. van Leeuwen (ed.),

V.R. Pratt, Modeling Concurrency with Partial Orders, Int. J. of Parallel Programming, 15, 1, Feb 1986, pages 33-71.

Another way of expressing trace equivalence, mathematically,
is to define the trace interpretation of a process.
The *trace interpretation* of process P is the
set of all traces of P,

Traces(P) = { t | P --t--> }Processes P and Q are trace equivalent if Traces(P) = Traces(Q).

Intuitively, trace equivalence compares processes according to what the
can do. It does not take into account what they can, at some
point, be in a position *not* do. For example, the processes

a.b.Halt --a-->--b--> /--a-->--b--> a.Halt + a.b.Halt / \ \--a-->are trace equivalent, because both can do a, both can do a followed by b, and neither can do anything else. In symbols,

Traces(a.b.Halt) = { epsilon, a, ab } Traces(a.Halt + a.b.Halt) = { epsilon, a, ab }However, these two processes might also be considered different because one may "refuse" to do b after doing a, while the other may not. More precisely, after doing a, the first process must be in a state where it is possible to do b, while the other may be in a state where it is not possible to do b. Informally, we might say that one may "deadlock" when run in the context

C[ ] = ([ ] | a'.b'.Halt)\abwhile the other may not.

Traces#(a.b.Halt) = { epsilon, a, ab } Traces#(a.Halt + a.b.Halt) = { epsilon, a, a#, ab }indicating that process a.Halt + a.b.Halt can do a and be in a state where it will no longer perform any additional actions.

This form of trace semantics can be extended to distinguish between different kinds of halting states. For example, we might identify a set of "deadlocked" process, and use different symbols at the end of traces to indicate whether a process has deadlocked or halted in a more desirable state.

/--a-->----b-->--c--> / --a-->----b-->--c--> / / \ /--c--> = trace = /-----b-->----c--> \--b-->/ \ \ \ \--d-->--e--> \ --b-->----d-->--e-->This normal form will be useful in comparing the interleaving approach with partial order semantics of concurrent processes.

The finer-grained forms of trace semantics using end-markers to identify termination states do not distinguish between different branching patterns within execution trees. For example, trace semantics will identify the following processes

/--b--> a.(b.Halt + c.Halt) --a-->/ \ \--c--> /--a-->--b--> a.b.Halt + a.c.Halt / \ \--a-->--c-->It seems that reasonable people might disagree on whether these two processes are equivalent. Perhaps the simplest way to see the difference between them is to assign a specific interpretation to a, b, and c. Since the essential difference between the processes lies in when they "make a decision" of "commit themselves" on whether to do b or c, it helps to choose an example where we can imagine a human being carrying out these actions. For example, let us consider

a = "I am going to the store" b = "I am going to buy some bubblegum" c = "I am going to buy some chocolate"Then the two processes may be interpreted as

a.(b.Halt + c.Halt) I am going to go to the store. When I get there, I am willing to either buy some bubblegum, or buy some chocolate. a.b.Halt + a.c.Halt I am willing to be convinced now to either go to the store and buy some bubblegum, or go to the store and buy some chocolate.The distinction is relatively subtle. However, the difference shows up when we execute either in parallel with the processes

Intuitively, Processes P and Q are bisimilar if, for all actions a,

if P --a--> P' then there is some Q with Q --a--> Q' and P',Q' bisimilar, and conversely,We can give a slightly more precise definition using bisimulation relations. A relation ~ on processes is a

if Q --a--> Q' then there is some P with P --a--> P' and P',Q' bisimilar.

if P --a--> P' then there is some Q with Q --a--> Q' and P'~Q'We say processes P and Q are

if Q --a--> Q' then there is some P with P --a--> P' and P'~Q'.

While the relationship to automata theory might suggest that there are efficient algorithms for deciding bisimilar, the automaton equivalence problem is only efficiently decidable for deterministic automata. The equivalence problem for nondeterministic automata, of the sort one usually obtains for processes, is pspace-complete. (The proof of pspace completeness uses a nondeterministic finite automaton to characterize the complement of the set of strings coding accepting computation sequences of pspace-bounding Turing machines.) See Kanellakis and Smolka for more information on connections between process equivalence and automata theory.

*Examples:*

- There is a bisimulation that relates the following two processes:
a.b.Halt ---a-->--b--> /--a-->----b--> a.b.Halt + a.(b.Halt + b.Halt) / \ /--b--> \--a-->/ \ \--b-->

This relation may be drawn as a set of vertical line segments between these two horizontal trees. (Or we may draw trees vertically and represent the simulation by horizontal arcs.) - There is no bisimulation between the following two processes:
/--b--> a.(b.Halt + c.Halt) ---a-->/ \ \--c--> /--a-->----b--> a.b.Halt + a.(c.Halt + b.Halt) / \ /--c--> \--a-->/ \ \--b-->

We can attempt to construct a bisimulation by drawning a vertial line segment between the roots of these trees. This leads us to draw two vertical line segments between processes produced after doing one a action. But the line to the upper branch of the lower tree fails to satisfy the condition of bisimulation. -
With recursive processes, the test for bisimularity
may be carried out on the finite dag presentation of the
infinite execution tree. For deterministic processes,
the test is like unification or finite automata equivalence.
For nondeterministic processes, it seems that a nondeterministic
version of the same algorithm works. However, I haven't been able
to find anything like this in the literature yet (* check again *).
The following two processes are bisimilar (if I haven't made a mistake):
|------c--------| | | V /--b-->| mu P (a. (b.c.P + c.Halt)) \---a-->/ \ \--c--> |-------a------| V | | /--b-->--c-->| |/ /\ a. (mu P (b.c.a.P + c.Halt) + c.Halt) ---a-->/ \--c--> \ \--c-->

The second graph here has unlabelled arcs, corresponding to epsilon moves in finite automata. This can be regarded as a notational convenience (when writing cyclic graphs for infinite trees), or epsilon moves can be removed by expanding the graph (see elimination of epsilon moves in finite automata).

DIGRESSION

Although we will not have time to discuss this in any detail, a useful way of restating the distinction between processes that "decide" at different stages in computation is through temporal logic. Temporal logic is an extension of ordinary propositional logic, with two operatorsEND DIGRESSIONS<> = possibly [] = necessarilya.(b.Halt + c.Halt) ??? how does HM logic work here ??? a.b.Halt + a.c.Halt ???

An interesting comparison with automata theory is that the determinization procedure for nondeterministic automata does not preserve bisimulation. In particular, we may regard

/--b--> a.(b.Halt + c.Halt) --a-->/ \ \--c--> /--a-->--b--> a.b.Halt + a.c.Halt / \ \--a-->--c-->as nondeterministic finite automata. Although they are not bisimilar processes, the standard determinization procedure produces the same deterministic automaton from either of these. The reason is that the determinization procedure only preserves trace equivalence.

For a concurrent program that might occur inside a larger program or system, a simple function from inputs to outputs is not enough to determine the behavior of the full system. In other words, if we want to use a concurrent process as a "black box", simple input-output behavior is not enough to reason about the behavior of the black box inside a larger system. This is illustrated by an example known as the Brock-Ackerman anomaly. (History: Kahn-MacQueen nets, etc.)

The Brock-Ackerman anomaly is an example with three parts, two sequential processes, P_1 and P_2, and a system, S, that can interact with either one. If we look at the mapping from sequences of inputs to sequences of outputs, the two processes P_1 and P_2 are equivalent. However, they behave differently when placed in the system S. This shows that mappings from inputs to outputs are not enough to determine the compositional behavior of processes in concurrent systems. More detailed information involving the dependencies between elements of the input sequence and elements of the outpus sequence are required.

Sink = in x. Sink D(nil) = in x. D(x::x::nil) D(x::l) = in y. D(y::y::x::l) + out x. D(l) Q_1 = in x. in y. out x. out y. Sink Q_2 = in x. out x. in y. out y. Sink P_i = Q_i | D(nil) L = in x. out_1 x. out_2 b.L Merge = in_1 x. out x. Merge + in_2 x. out x. Merge ---------- P_i: ---------------- S_i: | | | | | | V V | | V | --------- | | ----- | | Merge | | | | D | | --------- | | ------ | | | | | | V | | | | --------- | | V | | P_i | | | ------- | --------- | | | Q_i | | | | | ------- | --------- | | | | | L |------- | V | --------- ---------------- | VThe input-output function for P_1 maps a --> aa, ab --> aabb, ab --> abab, ..., abc --> aabbcc, ... This is also the input output behavior of P_2. The only difference is in the way that Q_1 and Q_2 respond to their inputs. When P_1 is given input a, the duplicator D sends a twice to Q_1. However, Q_1 does not output a twice until both inputs are received. In contrast, Q_2 may send a out once when it recieves the first a and then again when it received the second a.

Systems S_1 and S_2 differ on a single input a. In system S_1, input a is sent on to P_1, where it is duplicated and then sent to Q_1, which passes both messages on to L. Process L then sends a twice on the output channel, along with some output back to merge. However, since Q_1 is now the process Sink, further inputs to P_1 have no effect. Therefore, S_1 maps the input token a to the output sequence aa.

In system S_2, a is sent on to P_2, where it is duplicated. However, since Q_2 can send its first output a out before receiving the second input, it is possible for the first a to be sent along to L, which then sends b back along the feedback communication path. It is possible for this to come next through the merge operator, then down to D to be passed on to Q_2 before the second a leaves D. Therefore, one possible behavior of S_2 is to map the single input token a to the output sequence ab.

*Exercise:* Rewrite this in CCS using, for example, an atomic
action a for "send x on channel c" and a' for "receive x on channel c".
If you need to have two possible values on a channel,
you will need two possible atomic actions. For example,
if in x. P could read a or b, you will need to replace
in `x. P` by `a.[a/x]P + b.[b/x]P`, where
`[a/x]P` is the result of substituting a for x in P.

To begin with a concrete example, let us try to see how the two processes

a.Halt | b.Halt a.b.Halt + b.a.Haltmight be considered different. The first expression describes a concurrent system with two processes running in parallel. The two processes could be located anywhere in the world, or one on earth and one in space, for example. If physically separated, then an a action by one might have nothing to do with the b action by the other. One might occur before the other or, conceivably, they might in fact occur simultaneously. If we think of causality, then there may be no causal relationship at all. We might simply have a system where two unrelated events may occur independently.

In contrast, the expression `a.b.Halt + b.a.Halt` might describe a
single process that could either do one sequence of actions or the other.
There is a non-deterministic choice, but once the choice is made,
we appear to have a single process that performs two events in order.
We might even attribute causality, saying that if a.b.Halt occurs,
then the a event causes the subsequent b event.
There are lots of philosophical problems in defining causality in general.
However, it is possible to get some insight using a crude but pragmatic approach.
Specifically, let us say that action a causes action b,
in process or system, if it is not possible to do b before a.
With this view, the process a.b.Halt + b.a.Halt
chooses between an execution where a causes b and one where
b causes a, but does not allow independent execution.

A common way of accounting for the intuitive difference between a.Halt | b.Halt and a.b.Halt + b.a.Halt is to use partial orders of events. More specifically, in the execution tree interpretation, there are nondeterministic choices between sequential paths, with each tree trace equivalent to one with just a single nondeterministic choice at the beginning. Therefore, the execution tree model associates a set of linearly-ordered sequential behaviors with each processes. The partial order approach replaces each linearly ordered trace by a partially-ordered multiset (i.e., a set where an element may occur more than once) of actions. (* It isn't obvious how to incorporate the branching behavior that is considered important in bisimultion into the partial order model, but there might be some version of trees of partial orders (?) *)

Associating a set of partial orders with each process, we have

/--a--> a.Halt | b.Halt / \ \--b--> a.b.Halt + b.a.Halt { --a-->--b-->, --b-->--a--> }

In words, the first process has a single partially ordered trace, in which events a and b are unordered. The second process has two possible traces, one with a preceding b and one with the reverse order.

Some general advantages of partial orders are:

- Partial orders seem "philosophically correct" when processes are independent, possibly physically distant and especially when actions are assumed to take some duration. If two processes each take a millisecond, and the time intervals overlap, then we cannot safely assume that one occurs before the other. (If we did, we might overlap some important interaction between them.)
- Partial orders may be more convenient for certain applications. For example, the Rapide system at Stanford simulates the execution of a concurrent system and produces a partial order. The partial order produced by even a relatively small system may be very large, but it is still much smaller than the corresponding tree of possible interleavings. This is important for tools based on algorithms that search partial orders for certain error conditions, for example.
- The interleaving approach depends very heavily on assumptions about the atomicity of processes. If processes P and Q consist of atomic events a and b (respectively), then their possible interleavings are {ab, ba}. However, if we replace (in refinement) P and Q by processes that are composed of nonatomic events, then there interleavings become more complicated. This is a problem if we think of a process expression as a specification, to be realized by more complex processes with more specific behavior.
- There appear to be some useful operations on concurrent processes,
such as Pratt's
*orthocurrence*, which only make sense when we regard executions as partial orders.

*A partial order is characterized by its interleavings,*i.e., the set of linear orders consistent with the partial order. This is mathematically correct, as stated. However, the correspondence fails for partially ordered*multisets,*which is what actually occurs in practice. (* expand *)-
*Sets of strings have a nicer algebra,*namely, the algebra of regular expressions. While it is true that regular expressions are well-known, various researchers have been developing analogouos expressions and algebraic laws for sets of partial orders.