Process Equivalence in π-calculus

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₀ and the initial state of Q is Q₀,
then P simulates Q if P₀ simulates Q₀, 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.

1. 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.
2. 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.
3. 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).