Complete inference systems for weak bisimulation equivalences in the π-calculus

Abstract

Proof systems for weak bisimulation equivalences in the π-calculus are presented, and their soundness and completeness are shown. The proofs of the completeness results rely on the notion of symbolic bisimulation. Two versions of π-calculus are investigated, one without and the other with the mismatch construction. For each version of the calculus proof systems for both late and early weak bisimulation equivalences are studied. Thus there are four proof systems in all. These proof systems are related in a natural way: the proof systems for early and late equivalences differ only in the inference rule for the input prefix, while the proof system for the version of π-calculus with mismatch is obtained by adding a single inference rule for the version without it.