An automata based verification environment for mobile processes

Abstract

A verification environment for the π-calculus is presented. The environment takes a direct advantage of a general theory which allows to associate ordinary finite state automata to a wide class of π-calculus agents, so that equivalent automata are associated to equivalent π-calculus agents. A key feature of the approach is the reuse of efficient algorithms and verification techniques which have been developed and implemented for ordinary automata.