A Symbolic Procedure for Control Reachability in the Asynchronous π-calculus
Giorgio Delzanno · Electronic Notes in Theoretical Computer Science · 2004
We study the relationship between the asynchronous π-calculus and the specification language MSRNC combining multiset rewriting over first-order atomic formulas (MSR) and name constraints (NC) proposed in [ENTCS 50 (4) (2001)]. We exploit this connection to define a sound and fully automatic procedure for attacking control reachability for infinite-state specifications given in asynchronous π-calculus, i.e., for specifications of mobile processes with unbounded control, name generation, and name mobility.