Towards a Semantic-Based Verification Environment for the pi-calculus

A prototype version of a semantic-based verification environment for manipulating and analyzing mobile systems specified in the -calculus is presented. In the current version, the -environment provides two main facilities: a -calculus interpreter equipped with a graphical interface, and a verification tool which is used to decide (strong and weak) early and late bisimulation equivalences for finite -calculus processes. The -environment is built on top of existing verification systems, and the re-use of software modules, based on semantical considerations, is the key feature of our proposal. 1 Introduction The -calculus [MPW92] has become the best representative example of mobile process calculi, namely calculi in which the communication topology among processes can dynamically evolve when computation progresses. In the -calculus mobility is achieved via the communication of names rather than communication of processes as happens in so called higher order process calculi (e.g. ..