**Abstract.** Do process calculi have anything helpful to say about
web service choreography? Maybe. These slides are from a talk
for the w3c web-service choreography group. I've tried to
make the slides a 'primer', one that will help web-service-people
get an idea about what process calculi offer.

- piforweb-handout.pdf (83k, 5pages) - handouts from the talk
- piforweb.ppt (516k) - the slides themselves.

The remainder of this web page contains additional material and citations, more technical than was appropriate for the talk.

The easiest process calculus language is the pi calculus. Here is a minimal example:

proxy<y,"hello"> | !proxy(chan z,string s);z<s> }

The vertical bar separates to 'processes' (threads) which run in parallel. The first sends a channel-name and a string over the channel called 'proxy'. Meanwhile, in parallel, the second can receive such messages over the channel 'proxy', and sends them on. The exclamation mark means that it can keep handling further requests.

There's also a 'choice' command `x(a);C2 + y(b);C2` which can respond
either to x or to y. And a command `new x;` to
create a new channel. And that's it!

I think the pi calculus is a concise alternative to writing automatas. And also, when channel-names start getting passed around (like 'y' in the above example) then this is awkward to write in automata diagrams. But this is still speculation. People haven't written enough real programs in the pi calculus itself, yet, to know how good it is as a language.

- "The Pi Calculus" by Robin Milner. The first few pages of this book explain the calculus syntax.
- PICT, a single-threaded implementation of the pi calculus. http://www.cis.upenn.edu/~bcpierce/papers/pict/Html/Pict.html
- Join-Calculus, a subcalculus which is easier to implement than pi, and which has a "french" syntax. http://join.inria.fr/
- The Fusion Machine, a prototype distributed implementation of the pi calculus, in this Java applet: http://www.wischik.com/lu/research/fusion-machine

*Bisimulation* is a way to judge whether two programs
(or specifications) are equivalent. It involves paying attention
to the states of each, and to the possibilities still open at each state.
Let P, P' be the states in the left hand program, and Q, Q' be the states
in the right hand.

*A bisimulation S is a relation between states such that
whenever P S Q then:*

if state P can do an action to get to state P', then state Q must also be able to do the same action to end in some state Q', where P' and Q' are themselves related by S.

Basically, you draw the state diagrams of left and right programs. Then draw a set of lines to connect each state on the left to one on the right, and vice versa. (You can have many lines going from, or coming to, the same state). For every action that a left-hand-state can make, then all the equivalent right-hand-ones must also make, and the results must still be equivalent.

This definition is a very basic old one, back from the days of CCS. (CCS is an old process calculus from the 80s which doesn't allow you to pass channel-names as arguments. For more on it, read the book "Communicating and concurrent systems" by Milner.)

Bisimulation is symmetric. This makes you wonder: is it appropriate to use bisimulation to compare an implementation and a specification? Shouldn't we instead allow the implementation to do extra stuff?

You can partly fix this problem within bisimulation: by only comparing on those actions that are mentioned in the specification. That way, even if the implementation accepts a "extra-functionality" message and goes on to do something special, it still passes the bisimulation test.

You can fix the remainder of this problem with an asymmetric
version called *coupled
bisimulation*: a slightly more complicated definition that allows
the implementation more leeway. (In particular, it is allowed to
make a commitment step-by-step rather than all at once.)

- "Multiway Synchronization Verified with Coupled Simulation", a technical paper by Parrow and Sjödin. http://user.it.uu.se/~joachim/multiway.ps.gz.

Consider the program `u(x);x<"hello">;`. This receives
a channel-name, and then sends a message over it.
The question is, how do you account for this in bisimulation?
Here's one attempt:

*If P can perform the action u(x) and end in state P'
-- i.e. it receives the
formal argument x over channel u -- then the corresponding
state Q must also be able to receive an argument and end in Q'.
And also, P' and Q' must be equivalent no matter what actual
value was bound to x in them.*

This happens to be called "late bisimulation". It's a bit arbitrary,
because we picked the 'bind any value to x' clause out of the air. And indeed,
this bisimulation doesn't quite work. That is,
*it's possible for a client to distinguish between an implementation
and a specification, even when the implementation and specification are
late-bisimilar*.

The problem boils down to the fact that we're passing channels
as arguments in messages. And it's hard to define bisimulation
to account for this. So instead, researchers use a clear unambiguous
definition, called *congruence*...

*We say that a specification and implementation are congruent,
if no client can distinguish them*. This is a clear and unambiguous
definition, and it's clearly what we're aiming for. Problem is, it's
too hard to decide whether two programs are congruent. So, instead,
researchers try to find conservative approximations -- ones that
are overly-cautious, but at least they're practical!

- "The Pi-calculus: a Theory of Mobile Processes" by Sangiorgi. This book is the definitive tome on all the hundreds of different possible bisimulations, and on how they relate, and on congruences. A difficult read.
- "Open Bisimulation" is the efficient approximation that Sangiorgi came up with. It's in the book.
- "The Mobility Workbench" from Sweden is a tool for model-checking (and bisimulation-checking) on the pi calculus. http://user.it.uu.se/~victor/mwb.shtml.

Actually, even "congruence" isn't entirely unambiguous. It depends on what capabilities we allow for the clients, known as "contexts" in the literature. How much can the clients change during runtime? (reduction-closed vs shallow congruence). Can a client observe the system receiving a message, or only emitting a message? (synchronous vs asynchronous calculus). Can the client incorporate the program as an internal subroutine, or only access an existing already-running program? (full congruence vs equivalence). The first of these points turns out not to matter, but the rest of them lead to practically different definitions.

How does the complexity of the language relate to the complexity of bisimulation?

(1) The simplest calculus, CCS, has no reconfigurability at all. This has the easiest bisimulation.

(2) Then you add "internal mobility", which means you're only ever allowed to send the names of channels at the same time as creating them. The maths of this bisimulation is a bit harder, but not too much. The calculus here is called pi-I.

(3) Then you add "external mobility" aka "output capability", which means you can send the names of existing channels. This makes the maths of bisimulation more complicated. Biztalk does this, and the Join Calculus and Localised Pi Calculus. (which also have the ability to create fresh channels.)

(4) Then you add "input cabapility", which means that when someone tells you the name of an existing channel, you can receive messages over that channel. Bisimulation is the same complexity as above. The pi calculus has input capability, and also MS Highwire. People have avoided input capability in the past, on the grounds that it seemed too hard to implement. But recently, "fusions" seem to make its implementation possible.

- The pi-I calculus is by Sangiorgi. The paper for it is "On the expressiveness of internal mobility in name-passing calculi" by Boreale. (you need a subscription to Science Direct to download it.)
- Localised Pi Calculus is described in the paper "On asynchrony in name-passing calculi" by Merro and Sangiorgi. on-async.ps.gz
- Fusions are my research topic. An overview is here: www.wischik.com/lu/research/fusions.html