An automata based verification encironment for mobile processes

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. Work partially founded by CNR Integrated Project Metodi e Strumenti per la Progettazione e la Verifica di Sistemi Eterogenei Connessi mediante Reti di Comunicazione and Esprit Working Group CONFER2.