A Provably Correct Compiler for Efficient Model Checking of Mobile Processes.

We present an optimizing compiler for the π-calculus that significantly improves the time and space performance of the MMC model checker. MMC exploits the similarity between the manner in which resolution techniques handle variables in a logic program and the manner in which the operational semantics of the π-calculus handles names by representing π-calculus names in MMC as Prolog variables, with distinct names represented by distinct variables. Given a π-calculus process P, our compiler for MMC produces an extremely compact representation of P's symbolic state space as a set of transition rules. It also uses AC unification to recognize states that are equivalent due to symmetry. [ABSTRACT FROM AUTHOR]