A model checking algorithm for pi-calculus agents

This paper presents ?-logic, an action-based logic for ?-calculus. A model checker is built for this logic, following an automata-based approach. This is made possible by a result which allows finite state Labelled Transition Systems to be associated with a wide class of 7r-calculus agents by preserving a notion of bisimulation equivalence. The model checker was thus built reusing an efficient model checker for the action based logic ACTL, after a sound translation from 7r-logic into ACTL has been defined.