User:Fredokun/Pi calculus

The Pi-calculus is a Computer Science theory to describe and reason about concurrent and interactive systems. Such systems are composed of multiple agents capable of performing actions and also to communicate with other agents. Communications are transported through channels that may be moved among agents. This is why the Pi-calculus is often referred to as a theory of mobility.

The theory was initiated in the early 90's by Robin Milner (who received the famous ACM Turing award in 1999) and is based on his previous work on Concurrent systems (cf. the Calculus of Communicating Systems). It was further developped by many others and became an important topic in theoretical computer science.

As explained by Robin Milner himself (see An Interview with Robin Milner), there is no really good reason for the name of Pi-calculus (π-calculus) but the resemblance with the Lambda calculus is probably not accidental.

Technically, the Pi-calculus is a formal language in which the behavior of interacting agents can be expressed. The operational semantics explain the dynamics of the language, that is, how interactions can take place among agents. As a mostly theoretical work, the emphasis is put on the formal properties that can be extracted from the theory.

While we will mostly describe the original language proposed by Robin Milner, it should be noted that there exists in fact a whole family of similar languages or variants, usually referred as Pi-calculi. The variations occur either on syntactic or on semantic (and most often on both) aspects of the language. We will also describe some of the important variants in this article.

Overview

Let us discover the Pi-calculus on an example which illustrates the capacity of the language to express mobile systems. We are considering the abstraction of a mobile phone infrastructure. It is composed of mobile phones and relays as depicted on the following figure:

Infrastructure of Mobile phones and relays

In this example, we want to model the movement of mobile phones from relays to relays. On the figure, MPhone is connected to the relay named Relay. The phone's owner is moving towards another relay called NewRelay. At some point, the phone should switch from Relay (which gets farther) to the closer NewRelay, to obtain the following configuration:

Infrastructure of mobile phones and relays, after movement

To characterize the movement, we say that the mobile phone has been disconnected from the first relay and connected to the second one. So a relay can be either connected or disconnected.

Names and Processes

There are very few concepts to describe systems in the Pi-calculus. Basically, there are names and processes. The names are ubiquitous in the language. They roughly correspond to identifiers in programming languages, and are generally noted in lowercase such as myname, hello, and so on. While some variants introduce higher-level datatypes, names are the only values available in the pure Pi-calculus. Moreover, some names can be used to transport other names, they are then called channels. Processes represent the basic building blocks to describe the behavior of agents. One may compose process expressions either sequentially (using a simple dot .) or concurrently (using a vertical bar |).

We may now recast our mobile phone example in terms of Pi-calculus concepts. First, we will consider three different processes:

1. The MPhone process that expresses the behavior of a mobile phone
2. The Relay process for connected relays
3. The NewRelay process for disconnected relays

Mobile phones, as Pi-calculus processes, only manipulate names. They use a name com to receive/transmit information; com is thus a name employed as a channel.

Basic communication

Suppose for example that we would like to send a name hello using our phone through the channel com, we will write:

com!hello

Such basic construct is called an emission or action in the Pi-Calculus. We use here the syntax of the Pict programming language, which was the first programming language based on the Pi-calculus concepts. In the more traditional syntax, we would write:

${\overline {com}}\langle hello\rangle$

The Pict syntax has the advantage to be based on ASCII characters while keeping the concision and readability of the original syntax to express formal properties. That is why we use it in this article.

Complementarily, phones may get information through the same channel com which is expressed as follows:

com?(x)  (the ? disappears in the original syntax)

This is a reception or reaction. We can interpret the example above as a process listening on a channel com for some incoming information, characterized as x. This name x is said to be a bound name, it must be substituted by the received information (another name) when the communication occurs. To illustrate this particular point, let us take a simple example of two communicating processes. The program, referenced as [1], is as follows:

com!hello.com?(x) | com?(y).com!y   [1]

The vertical bar | is used to separate concurrent processes. The process on the left is composed of a sequence of two operations. The first one com!hello emits the name hello via the channel com. A reception on com follows. The action on the left is said to be in prefix position (or simply a prefix) and what follows is a continuation of the process. The process on the right first listens on com and then reemits the same information (using the bound name y) on the same channel. This is thus something like an echoing process.

Communications take place synchronously in the Pi-calculus. This means that both an emission prefix and a reception prefix must be matched for the information exchange to take place. In our previous example, such matching occurs, and we obtain the following configuration:

com?(x) | com!hello    [2]

The passage from [1] to [2], which informally corresponds to the execution of the program and is more formally defined as a reduction or a silent transition can be decomposed in two steps. First, both the communication prefixes "disappeared" in [2]. This means that they have been executed. Then, the bound name y has been substituted with the communicated name hello in the continuation of the process on the right. Anticipating on the formal developments, this one-step execution is formally noted as follows:

${\begin{matrix}&\tau &\\com!hello.com?(x)|com?(y).com!y&\longrightarrow &com?(x)|com!hello\end{matrix}}$

Behavior abstractions

We describe first a basic behavior for mobile phones that regularly emit some fixed information (named beep). This behavior is written as follows:

MPhone0()= com!beep.MPhone()                     

We use a construct called abstraction which allows to name behavior definitions, here MPhone1. It is then possibe to use this name within the behavior (or any other behavior) to model calls and recursion. This is similar to function definitions and function calls in other programming languages.

So we model here a process that emits a beep on a channel com and reiterates indefinitely the same behavior.

Such abstractions are not part of the pure Pi-calculus mostly because they complicate the formal treatment of the language. However they can be encoded easily and are simpler to understand that the more primitive replications (defined later on). Sometimes (as in the Introduction to the Pi-calculus by Joachim Parrow), the construct is provided in the core language.

Relays, either connected or disconnected, are also described as processes using names and channels as basic constructs. Before a communication can take place, a relay must inform the mobile phone that it is available. For this, the relay sends some information on a channel named avail. We can abstract the behavior of a connected and available relay as follows:

RelayOk(com,avail)= avail!com.com?(x).Relay(com,avail)

To signal to a connected mobile phone that the relay is available, we send the communication channel com on the availability channel avail. We thus take advantage of the possibility of sending channels over channels. A phone may only use com if it can receive it through avail. We then wait for some information on channel com and reiterate a general relay behavior. We can see here that behavior abstractions may be parameterized (here by two name com and avail). To simulate this in the pure calculus, we have to use extra communication.

Choice operator and nondeterminism

The global (connected) relay is either available (as detailed above) or not available. In the latter case, we may simply consider the relay "out of order". This may be expressed using the inert processed noted 0. So the relay behavior is either RelayOk or 0. Since we do not want to model why a relay becomes unavailable, we would like the choice to be nondeterministic. The Pi-calculus introduces + the sum operator or choice to that end. So the complete connected relay behavior is as follows:

Relay(com,avail) =   RelayOk(com,avail)      // either available 
                   + 0                       // or not

The previous definition for the mobile phone does not check if a relay is available or not. We can update the definition as follows:

MPhoneAvail(avail,relink)= avail?(com).com!bip.MPhone(avail,relink) 

Now the mobile phone only works if the relay is available. The use of the relink channel is explained in the next section.

Restriction and Scope extrusion

The last objective of our specification is to model the dynamic change of relay. For this we have to model the behavior of disonnected relays. Such relay do not do anything except when a new connection is requested (e.g. when a mobile phone approaches the relay). For this we introduce a specific channel named relink. The behavior of disconnected relays is as follows:

NewRelay(relink)= new(com) new(avail) relink!avail.Relay(com,avail)

First, we create dedicated communication and availability channels, using the restriction operator new (Ν in the original syntax). Intuitively, this operator creates a new and unique name. Uniqueness will be provided through the renaming of the created name if there exist conflicting names (this is to satisfy what is called Α-equivalence in the lambda-calculus). Note that new has a special status in the Pi-calculus. It is a binder for a fresh name that allows scope extrusion. This means that new(x) introduces a scope for the created name (x or a new name is x already exists); and it is then possible to "change" the scope of x under some circumstances. Parentheses are used to explicit the scope of a name. By default, the introduced scope goes from the new> construct to the next parallel construct |. For example, in:

new(x) P | Q

The name x has scope P, or is restricted to P. But if x does not appear in Q, then we can extrude its scope as follows:

new(x)( P | Q )

Now the scope of x extends to both processes P and Q

This is perhaps the most unique feature of the Pi-calculus. But in our illustrative example, we will interpret the new construct as a simple channel creation.

To handle the change of relay in mobile phones, we add a behavior in case of reconnection; this is as follows:

MPhoneRelink(relink) = relink?(avail).MPhone(avail,relink)

When a new relay activates relink, then we fetch the new avail channel and reiterate the mobile phone behavior. This global behavior becomes:

MPhone(avail,relink) =   MPhoneAvail(avail,relink) 
                       + MPhoneRelink(relink)

References (external links)

• http://move.to/mobility/ : A page about the Pi-calculus and other mobile calculi