Before moving on, there's one question that I thought was important enough to promote up to the front page, instead of just answering it in the comments. A commenter asked about process replication, !P, wanting to know if it terminates.

The answer comes in two parts.

- !P does process creation
*on demand*. It's not an infinite parallel group of processes; it's just a way of writing that there are as many of P as you need. So you can think of it like tape cells in a Turing machine: we never say that a Turing machine tape is infinitely long; but there's always*enough*cells. !P isn't an infinite replication of P; it's a notation for "enough copies of P". So when you're done using replicas of P, you can think of !P disappearing. - Often in π-calculus, we actually don't worry about termination of every process. You can think of it in terms of garbage collection: we're running some group of processes to perform a computation. When they're done, they terminate. Any process which has no ports that are reachable by any other active process can simply be collected.

The next place to go in our exploration of π-calculus is considering just what it really means for two processes to be equivalent. The fundamental equivalence relation in

π-calculus is called *bisimulation*. The idea of bisimulation is roughly a kind of observational equivalence: two processes are equivalent under bisimulation if they exhibit the same visible behavior under all tests by an external observer.

Consider two processes, P and Q. The *only* thing that an external observer can see are the *communication channels* that are not localized to the processes. So the first requirement for P and Q to be equivalent is that they have equivalent externally visible communication channels.

We need to look a bit more in detail at that first requirement. What does it mean for communication channels to be equivalent? Given two channels x and y, they are equivalent if they can be used to send exactly the same messages. So far, in our examination of π-calculus, we've used a fully general notion of channels - any channel can be used to send or receive any message. But as we move on, we'll be starting to use typing. So two channels will be equivalent if they have the same *type*; and the definition of the type of a channel will be a list of the kinds of messages that can be sent and received using the channel. (To keep things simple, we'll assume that channels are *symmetric*, meaning that any process that can use a channel can use it to send or receive (or both) any message supported by the channel.)

So now we get to the difficult part.

From the outside of the process, observing the process, we can view it as a kind of state transition system. What that really means is that we can send it a message, and then watch what happens after it receives it: to be specific, what messages it sends in response.

So given a process P with *n* communication channels

C_{P}=c_{p1}...c_{pn}, we'll model it as a state machine. So, when the process

is first created, we'll say it's in state S_{P0}. Each time it receives a message,

it will take a transition to a new state depending on which channel received the message,

and what the content of the message was. When it makes the transition, it can also*generate* a sequence of messages. So for each transition, we need to specify an

initial state a message as input, and a target state and a sequence of messages as output.

So for a process P, we'll define the following types:

- S
_{P}is the set of states of P - C
_{P}is the set of channels of P - M
_{P}is the set of pairs (c,m) where c∈C_{P}, and m is a message that can be send using c

With that set of type definition, we can say that the *transition relation* for

P is a relation T : (S_{P}×M_{P}) → (S_{P}×Sequence(M_{P})) - that is, a *relation* from a state of P and an input message to a new state of P and a sequence of messages generated by the transition. The fact that it's a *relation* is very important: there can be more than one possible transition from P on a given message.

Suppose we have two processes P, with transition relation T_{P} and message set

M_{P}, and Q with transition relation T_{Q} and message set M_{Q}

We'll say that P in state P_{i}*simulates* Q in state Q_{j} if

M_{Q}⊆M_{P}, *and* for every message m ∈ M_{Q},

T_{Q}(Q_{j},m) and T_{P}(P_{i}) generate the *same*

sequence of messages on corresponding channels. (I'll gloss over the formality of defining corresponding channels; I'm sure you can use your intuition to figure out what it means.)

Now, here's where it gets tricky.

Suppose I have a state Q_{x}. Given a message m, there is some *set* of

states Q_{x}(m) that it could transition to. We can take the *union* of the states in Q_{x}(m) - Q_{x}^{∪}(m). Now, T_{Q}(Q_{x}^{∪}(m), n) - that is, the transition relation from the set of possible targets to T_{Q}(m) given message n - is the union of T_{Q}(q,n) for all q∈Q_{x}^{∪}(m). A *set of states* of P simulates a set of states of Q if the simulation relation as defined for single states works for the union-states when their transition sets are unioned.

If the initial state of P is P_{0} and the initial state of Q is Q_{0},

then *P simulates Q* if P_{0} simulates Q_{0}, and for all possible transitions from *the set of states* Q_{i} to the *set of states* Q_{j} triggered by message m, there is some pair of *sets of* states P_{k} and P_{l} such that P_{k} can transition to P_{l} on message m, *and* P_{k} simulates Q_{i} and P_{l} simulates Q_{j}.

Whew. That's a mouthful. (Or a keyboardful, or whatever...) All of that is a

formal way of saying that for all *sequences* of messages that can be received by Q, P and Q will make transitions that generate the same outputs. Note that this is not yet symmetric: P *can* have messages not supported by Q, and it can do anything it wants when it receives one of its messages. But if someone has processes P and Q, then they cannot possibly distinguish them by sending messages that both processes can understand.

Now that that's out of the way, the next step is easy. P and Q are equivalent under bisimulation if P simulates Q and Q simulates P.

So let's look at one or two of the things that we've seen before, and see if they're equivalent under bisimulation.

- P={?a(x).F(x)+?a(x).G(x)} and Q={?a(x).{F(x)+G(x)}}. Are these equivalent? Yes. Even though P commits earlier than Q does, there is no way for an external observer to determine when it make a commitment to F or G.
- P={?a(x).F(x)+?a.G(x)}, Q={?a(x).(F(x)+G(x))}. These are equivalent, for the same reason as above: there's no way to tell when the commitment to F(x) or G(x) happens.
- P={?a(x).(F(x)|G(x))}, Q={?a(x).F(x)|?a(x).G(x)}. Are these equivalent? In general, no, these are
*not*equivalent. In P, sending one message to a will start both F(x) and G(x); in Q, sending one message to a will start F(x)*or*G(x).

- Log in to post comments

I'm sorry but I didn't understand one thing: what's the difference between properties 1 and 2 ?

Aren't Q={?a(x).{F(x)+G(x)}} and Q={?a(x).(F(x)+G(x))} the same thing?

Daniel:

Definitely a typo. I have to try to remember what the second example was

supposedto be, and then I'll fix it :-).I guess you never got around to fixing the second example. Too bad this isn't a wiki, we could fix typos and such for you (though I guess a wiki comes with its own set of problems).

My guess:

2. P={?a(x).F(x)|?a(x).G(x)} and Q={?a(x).F(x)+?a(x).G(x)}

For P either F or G could run when something's written to a, same as for Q.

I wonder though if example 1 holds if F and G take a while to run and I write to "a" in quick succession. Q won't be able to read off "a" until F or G is done. For P, with ?a(x).F(x) busy, would ?a(x).G(x) get picked? If so, then they're not equivalent.

P.S. you seem to be using () and {} interchangeably for grouping. Are they?