• What PiET is?

• What are the equivalences available for the pi-calculus?

• What equivalences are checkable with PiET?

• Technical informations about Piet

• A very quick tutorial.

• Some working examples.

• Download PiET.

• Contact Me!

What PiET is?

PiET stays for Pi Calculus Equivalences Tester.
It is a very minimal tool to check ten types of behavioural equivalences for the pi-calculus [1].
PiET is composed by two part:

1. The kernel part that is a shell program.

2. A very simple GUI that make the use of PiET easier.

While the kernel can be used without the GUI, the latter is completely useless without the kernel part.

PiET (kernel) is completely written in Fresh Ocaml [2]. This language extends Ocaml by primitives for a simpler encoding of names and simpler check of alpha-equivalences among processes.
PiET is distributed under the LGPL licence.
In this pages both binaries and sources are available.

What equivalences are checkable with PiET?

The theory of pi-calculus has today (2006) more than 15 years. In this time different behavioural equivalences were proposed with very different properties.
Each equivalence has two possible definitions depending on how we want to treat tau actions. If we consider them like others we obtain the Strong version of the equivalence. If we prefer to ignore tau actions than we obtain the Weak versions.

The Weak Barbed Congruence [3] is the principal behavioural equivalence for the pi-calculus. But it's, in the general case, hard to check since it involves a quantification over all possible contexts.

Others equivalences have been proposed as techniques to prove Barbed congruence. Here we recall the most important:

• Early Equivalence

• Early Congruence

• Late Equivalence

• Late Congruence

• Ground Equivalence

• Ground Congruence

• Open Congruence

All of them has, as before stated, both the Strong and the Weak versions.

Early, Late and Ground Equivalences are bisimulation relations. But they are not congruences. Their corresponding congruences are obtained with a closure over all contexts.
To the contrary the Open relation is a Congruence expressed directly in terms of bisimulation that doesn't need a closure over all contexts. It has also a very efficient characterization that allow an efficient implementation.

The following graph represent the inclusion order between the different relations (weak and strong version have the same order):

So the Early Congruence, Ground Congruence and Barbed Congruence coincide (both Strong and Weak versions).
The Early Congruence is the main auxiliary relation to check Barbed Congruence.
Late congruence is also very important and widely studied.
The open bisimulation is smaller (in both Strong and Weak version) than Barbed (i.e. Early and Ground) Congruence.
But since it allows a good theoretical presentation in term of bisimulation and also an efficient characterization it is the most used behavioural relation in practise.

For a serious introduction to the theory of behavioural equivalences for the pi-calculus see [3].

What equivalences are checkable with PiET?

There are two very good tools for checking open bisimulations:

1. The Mobility Workbench [4].

2. The ABC [5].

Both are mature and very fast and use the (symbolic) characterization of Open bisimulation.

PiET doesn't check Open bisimulation (other tools would be surely better).
The main objective of PiET is to offer an ambient to check all other equivalences.

What PiET can check is:

• (Strong/Weak) Early Equivalence

• (Strong/Weak) Late Equivalence

• (Strong/Weak) Early Congruence

• (Strong/Weak) Late Congruence

• (Strong/Weak) Ground Equivalence

So PiET can check 10 types of equivalences.
Ground Congruence is not present in the list because it coincide with the Early Congruence for both the Strong and Weak versions.

Technical informations about PiET

PiET implements the ideas developed by H. Lin in [6,7].
The symbolic semantic for the pi-calculus proposed in [6] has an efficient characterization described in [7].
PiET uses the ON-THE-FLY algorithm described in [7] using efficient data structures like hash tables and some heuristics to improve performances.

A very quick tutorial

This sections provide a very quick tutorial to get you start working with PiET.
I assume that you use the PiET GUI (if it is not true read anyway, at the end all should be clear also for the use without the GUI).

If you have not the time to read all this tutorial you can try to use PiET examples contained in the GUI and learn by yourself (it is very very easy). They are available viewing the Syntax Help window in PiET.
Click Help/Syntax Help.

First of all launch the PiET GUI (Make sure you have Java 2 installed!!).
Since the GUI is a jar file this can be done by a simple double click in most systems. However you can always use the following command:

java -jar PiETgui.jar

The GUI is very minimal. It offers two text areas. The biggest is the edit area where you will edit your file containing the definitions of pi-calculus processes. The smallest, at the bottom, is used to display the output.
The menu bar in the top has a list-box (where you select the equivalence to test), a button "TEST" (click it to start the test) and a disabled button "STOP" (it will activate during the computation).
In the Edit menu there is the Settings item.
In the Help menu there is the Syntax Help item. Use it to view the syntax description and some examples.

In the setting menu there are 4 parameters to set. The path of the kernel, the state space limit (that is the maximum number of pi-calculus different states to be visited), the compositional heuristic flag and the print relation flag. While the meaning of the print relation flag is self explanatory (it displays the computed relation without identities), the compositional heuristics must be explained. The compositional heuristic works as follow:

The compositional heuristics works only when computing equivalences different from (Strong and Weak) Ground Equivalence.
We say that P~Q iff P and Q are structural congruent or if PiET has previously found that they are equal regarding the selected behavioural equivalence (that is not a Ground equivalence).
Now if we are trying to equate the processes P = R1 | P1 and Q = R2 | Q2 with R1~R2 than we first check if P1 equates Q1. If so we have a proof that P equates Q because all the equivalences (except the Ground) are preserved by parallel composition. Instead, if P does not equate Q, we simply check the equivalence of P1 and Q1 in the standard manner.
A practical example of the convenience of this heuristic in some cases is presented in the example 5 of the examples section.

Now we can say that the use of PiET is essentially the following:

1. Write the input in the text area.

2. Open the Settings windows and set the parameters as you want.

3. (Save the file and) Click the "TEST" button.

4. Wait until the answer appear in the text area in the bottom, or click the "STOP" button.

5. Return to 1.

So what you need to know is HOW to write the input.
The syntax for the input is defined by the following grammar:

KEYWORDS: AGENT | LIST | TEST | WITH 
name (a,b,x,y,...): [a..z] [a..z + A..Z + 0..9 + '_']*
def_name (A,B,P,Q,...): [A..Z] [a..z + A..Z + 0..9 + '_']*
name_list ::= 
         name            |
         def_name        |
         name, name_list |
         def_name, name_list 
Processes (p,q,r,...) ::= 
         p | p                    | (* par operator *)
         !p                       | (* bang operator *)
         def_name(name_list)      | (* call of a definited process *)
         def_name                 | (* costant process *)
         def_name[name_list]      | (* costant process with some free names *)
         ^name_list p             | (* names restrictions *)
         m                          (* guarded sum *)
Guarded sum (m,n,...) ::= 
         0                    | (* inactive process *)
         prefix.p             | (* prefixed process *)
         prefix               | (* synctactic sugar for prefix.0 *)
         (m + m)                (* guarded sum (need parenthesis) *)
Prefixes (a,b,...) ::= 
         _t                | (* tau *)
         name(name)        | (* input action *)
         name()            | (* synct sugar for name(x) with x fresh *)
         name<name>        | (* output action *)
         name<>            | (* synctactic sugar for _t.(^x name<x>) *)
         [name=name]a      | (* match *)
         [name#name]a        (* mismatch *)
(**************************************************************************************
POLIADICITY: Poliadicity is supported by a translation ( [[ _ ]]: polyadic -> monadic ) 
to the monadic form. It is applied when input or output prefixes with more than one 
object are used. No detection of runtime error (different ariety of channels) is 
supported in this release.
         
         [[ name(a1,...,an) ]] = name(x).x(a1).x(a2). ... .x(an)
         [[ name<a1,...,an> ]] = _t. ( ^x name<x>.x<a1>.x<a2>. ... .x<an> ) 
***************************************************************************************)
definitions ::=
         proc_definition definitions
         
proc_definition ::=
         AGENT def_name () := proc ;   |
         AGENT def_name (name_list) := proc;
(***************************************************************************************
NOTE: all free names of the definied process must be included in the list          
of formal names of the definition. 
Example 1: AGENT P(x) := x<a>.0 is NOT a correct definition since a is free.
Example 2: AGENT P(a,x) := x<a>.0 is a correct definition.
***************************************************************************************)
list_definition ::= 
         LIST def_name := name_list;
(***************************************************************************************
NOTE: This declaration may be usefull when there are several process definitions using 
the same names. As an example the two following definitions 
AGENT P(x,y,z,w,r,s):= x<y>.z<w>.r<s>;
AGENT Q(x,y,z,w,r,s,t):= x<y>.z<w>.r<s>.t(v).P(x,y,z,w,r,v);
can be rewritten to
LIST L := x,y,z,w,r;
AGENT P(L,s):= x<y>.z<w>.r<s>;
AGENT Q(L,s,t):= x<y>.z<w>.r<s>t(v).P(L,v);
****************************************************************************************)

Piet_directive ::=
         TEST proc WITH proc ;;
Piet_document ::=
         definitions Piet_directive |
         Piet_directive

Syntax presented above must seem difficult but it is really not.
The user only need to remember 4 important things:

1. PiET uses the Guarded Sums version of the pi-calculus. So you can't write processes as: (^x.a<x>.0 + a<b>.0) because the first operand of the sum is not a prefixed process.

2. Guarded sums need to be well-parenthesized. So you can't write processes as: (a<b>.0 + c<d>.0 + e<f>.0).

3. If you like to use the abbreviations for output prefix x<> please note that the translation is the following:
   a<> = _t.(^x a<x>)
   and not, as usually assumed,
   a<b> = ^x a<x>.

4. PiET implements poliadicity with a translation to the monadic form. So if you use poliadic communications always remember how they are translated.

Some working examples

Example 1: this example defines a simple single state process Bang and sets the verification between Bang and a process defined using the bang operator.

You can try to check what equivalence equates the two process (all ! ).

Example 2: This example shows that Late Equivalence and Early Equivalence don't coincide. This example comes from [3].

Now check if they are strong late equivalent or congruent (no!) or strong early equivalent or congruent (yes!).

Example 3: This example is a simple instance of the Expansion Lemma.

Example 4: This is a more complex example. Buf2 and Buf22 are two 2-phases buffers. This examples comes form [5].

Now check if Buf2 and Buf20 are weak early related (yes!).

Example 5: This example shows how the Compositional Heuristic can works well in particular cases (and this is an extreme one !).

Now try to check the two process P1 and Q1 without the compositional heuristic. Of course they are equal because their components (P and Q) are early congruent (proved in example 3).
If you are using the default state space limit (1000) than PiET will alert you that it is too small to verify the two process.
Using a greater limit PiET will terminate (on my computer in about 30 sec) equating the two processes.
Now try to use the compositional heuristics. You will see the difference!

Download PiET 1.0 (Updated 28 September 2006)

If binaries for your platform are not available you can try to install Fresh Ocaml (with the native code compiler!) in your system and compile the kernel following the instructions contained in the sources package. Fresh Ocaml is available here. The compiled Gui (a jar file) should works well in every Java compatible system.

Contact Me!

Feel free to contact me for every reasons.
My e-mail is: miomatteo@gmail.com .
My personal home page is www.dimi.uniud.it/mio .

References:

1. R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes (parts I and II). Information and Computation,
   100(1):1--77, 1992.

2. M.R. Shinwell and A.M. Pitts, Fresh Objective Caml User Manual. Cambridge University Computer Laboratory,
   February 2005. Website: http://www.fresh-ocaml.org/ .

3. Davide Sangiorgi, David Walker: The Pi-calculus: A Theory of Mobile Processes, Cambridge University Press,
   ISBN 0-521-78177-9.

4. B. Victor. A Verification Tool for the Polyadic pi-Calculus. Licentiate thesis, Department of Computer Systems,
   Uppsala University, Sweden, May 1994. Website: http://www.it.uu.se/research/group/mobility/mwb .

5. ABC: Another/Advanced Bisimulation Checker. Website: http://lampwww.epfl.ch/~sbriais/abc/abc.html .

6. H. Lin, Symbolic Bisimulations and Proof Systems for the pi-Calculus. Kyoto, Japan, July 1996.

7. H. Lin, Computing Bisimulations for Finite-Control pi-Calculus. Journal of Computer Science and Technology, Vol.15, No. 1, 2000.