## The Mobility Workbench: A Tool for the Pi-Calculus

**Björn Victor and Faron Moller**
*Abstract:* In this paper we describe the first prototype
version of the Mobility Workbench (MWB), an automated tool for
manipulating and analyzing mobile concurrent systems (those with
evolving connectivity structures) described in the pi-calculus. The
main feature of this version of the MWB is checking open
bisimulation equivalences. We illustrate the MWB with an example
automated analysis of a handover protocol for a mobile telephone
system.

*Extract from the user's manual:* The Mobility Workbench
(MWB) is a tool for manipulating and analyzing mobile concurrent
systems described in the pi-calculus, developed by Faron Moller and
Björn Victor, in collaboration with Davide Sangiorgi at the
University of Edinburgh. It is written in Standard ML, and
currently runs under the New Jersey SML compiler.

In the current prototype version, the basic functionality is to
decide the open
bisimulation equivalences of Sangiorgi, for agents in the
monadic pi-calculus with the original positive match operator. This
is decidable for pi-calculus agents with finite control,
correlating to CCS finite-state agents, which do not admit parallel
composition within recursively defined agents.

The algorithm is based on the efficient characterization of the
equivalence described in [Sangiorgi 1993], and
(necessarily) generates the state space ``on the fly''. Versions
for both the strong and weak equivalences are implemented. There
are also commands e.g. for finding deadlocks and interactively
simulating an agent.

The MWB is undergoing constant and dynamic changes. This guide
describes the prototype version, but
we are currently developing a new version with efficiency in focus,
which supports the polyadic calculus, handles sorts, and has model
checking commands.

*LFCS report ECS-LFCS-94-285,
February 1994.*

Previous |

Index |

Next