Process Equivalence in π-calculus

Apr 23 2007 Published by under Pi 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
CP=cp1...cpn, we'll model it as a state machine. So, when the process
is first created, we'll say it's in state SP0. 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:

  • SP is the set of states of P
  • CP is the set of channels of P
  • MP is the set of pairs (c,m) where c∈CP, 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 : (SP×MP) → (SP×Sequence(MP)) - 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 TP and message set
MP, and Q with transition relation TQ and message set MQ
We'll say that P in state Pi simulates Q in state Qj if
MQ⊆MP, and for every message m ∈ MQ,
TQ(Qj,m) and TP(Pi) 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 Qx. Given a message m, there is some set of
states Qx(m) that it could transition to. We can take the union of the states in Qx(m) - Qx(m). Now, TQ(Qx(m), n) - that is, the transition relation from the set of possible targets to TQ(m) given message n - is the union of TQ(q,n) for all q∈Qx(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 P0 and the initial state of Q is Q0,
then P simulates Q if P0 simulates Q0, and for all possible transitions from the set of states Qi to the set of states Qj triggered by message m, there is some pair of sets of states Pk and Pl such that Pk can transition to Pl on message m, and Pk simulates Qi and Pl simulates Qj.

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).

No responses yet

  • Daniel says:

    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?

  • Mark C. Chu-Carroll says:

    Daniel:
    Definitely a typo. I have to try to remember what the second example was supposed to be, and then I'll fix it :-).

  • jag says:

    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?

Leave a Reply