This thesis describes the polyadic version of the Mobility Workbench (MWB), an automated tool for manipulating and analyzing mobile concurrent systems (those with evolving connectivity structures) described in the polyadic pi-calculus. The main feature of this version of the MWB is checking open bisimulation equivalences, and doing so with efficiency in mind.
The open bisimulation equivalences are described in a polyadic setting, and efficient characterisations of both the strong and the weak equivalences are presented and proven to coincide with their standard formulations.
The equivalence checking algorithm, which by necessity generates the state space ``on-the-fly'', is presented in detail and proven correct. Aspects of the implementation of the tool are described in some detail, for example the representation of pi-calculus agents using de Bruijn indices.
We illustrate the MWB with an example automated analysis of a handover protocol for a mobile telephone system.
DoCS Licentiate thesis 94/50, May 1994 (Postscript version, compressed)
MWB Web page
MWB distribution directory
@PhdThesis{vic:lic,
author = "Bj{\"o}rn Victor",
title = "A Verification Tool for the Polyadic $\pi$-Calculus",
school = "Department of Computer Systems, Uppsala University, Sweden",
year = "1994",
month = "May",
type = "Licentiate thesis",
note = "Available as report {DoCS 94/50}"
}