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)\ab
while 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 a'.b'.Halt.
The second process above could deadlock with a'.b'.Halt,
but the first one will not.
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 bisimulation if, whenever P~Q the following two conditions are satisfied:
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 bisimilar if there is some bisimulation ~ with P~Q. This is very similar to the relations used to represent expression equivalence on graph representations of symbolic expressions (see [Paterson and Wegman; Dwork, Kanellakis and Mitchell]) and the relations used to represent equivalence of deterministic finite automata (see [Aho, Sethi and Ullman; Hopcroft and Ullman]).
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:
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.)
/--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.
|------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).
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 ???
/--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 | ---------
---------------- |
V
The 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.Halt
might 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: