A Symbolic Semantics for the pi-calculus

Symbolic transition systems are used as a basis for giving a new semantics of the π-calculus. This semantics is more amenable to automatic manipulation and sheds new light on the logical differences among different forms of bisimulation over dynamic process algebras. Symbolic transitions have the form (Formula Presented), where, intuitively, ø is a boolean constraint over names that has to hold for the transition to take place, and α is π-calculus action; e.g., [x = y ]α. (Formula Presented) says that action α can be performed under any interpretation of names satisfying x = y. A symbolic bisimulation is defined on top of the symbolic transition system and it is shown that it captures the standard ones. Finally, a complete proof system is defined for symbolic bisimulation.