
PiET Pi Calculus Equivalences Tester Version: 1.0 
Author: Matteo Mio 
PiET stays for Pi Calculus Equivalences
Tester.
It is a very minimal tool to check ten types of
behavioural equivalences for the picalculus [1].
PiET
is composed by two part:
The kernel part that is a shell program.
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 alphaequivalences 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 picalculus 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 picalculus. 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 picalculus see [3].
What equivalences are checkable with PiET?
There are two very good tools for checking open bisimulations:
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 picalculus proposed in [6]
has an efficient characterization described in [7].
PiET
uses the ONTHEFLY algorithm described in [7] using
efficient data structures like hash tables and some heuristics to
improve performances.
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 picalculus processes. The smallest, at the bottom, is
used to display the output.
The menu bar in the top has a listbox
(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 picalculus 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:
Write the input in the text area.
Open the Settings windows and set the parameters as you want.
(Save the file and) Click the "TEST" button.
Wait until the answer appear in the text area in the bottom, or click the "STOP" button.
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:
PiET uses the Guarded Sums version of the picalculus. 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.
Guarded sums need to be wellparenthesized. So you can't write processes as: (a<b>.0 + c<d>.0 + e<f>.0).
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>.
PiET implements poliadicity with a translation to the monadic form. So if you use poliadic communications always remember how they are translated.
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.
(* this is a comment!!! *) 
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].
AGENT A(x,y) := ( x() + x(z).z<> ); 
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.
AGENT P(a,b,c) := a(x).0  b<c>.0; TEST P(a,b,c) 
Example 4: This is a more complex example.
Buf2 and Buf22 are two 2phases buffers. This examples comes form
[5].
LIST L := i,o; 
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 !).
(* First redefine the 2 processes of example 3*) TEST P1(a,b,c) 
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)
Binaries for Linux x86 

Binaries for MacOSX ppc 

Binaries for MacOSX intel 
Since there is no version of Fresh Ocaml for MacOSX intel you have to use the ppc version emulated with Rosetta. 
Binaries for Windows 
Still not available 
Sources of the kernel part (fresh ocaml) 

Sources of the GUI (java) 
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.
Feel free to contact me for every
reasons.
My email is: miomatteo@gmail.com
.
My personal home page is www.dimi.uniud.it/mio
.
References:
R. Milner, J.
Parrow, and D. Walker. A calculus of mobile processes (parts I and
II). Information and Computation,
100(1):177, 1992.
M.R. Shinwell and
A.M. Pitts, Fresh Objective Caml User Manual. Cambridge University
Computer Laboratory,
February 2005. Website:
http://www.freshocaml.org/
.
Davide Sangiorgi,
David Walker: The Picalculus: A Theory of Mobile Processes,
Cambridge University Press,
ISBN 0521781779.
B. Victor. A
Verification Tool for the Polyadic piCalculus. Licentiate thesis,
Department of Computer Systems,
Uppsala University, Sweden, May
1994. Website: http://www.it.uu.se/research/group/mobility/mwb
.
ABC: Another/Advanced Bisimulation Checker. Website: http://lampwww.epfl.ch/~sbriais/abc/abc.html .
H. Lin, Symbolic Bisimulations and Proof Systems for the piCalculus. Kyoto, Japan, July 1996.
H. Lin, Computing Bisimulations for FiniteControl piCalculus. Journal of Computer Science and Technology, Vol.15, No. 1, 2000.