On the benefits of using the up-to techniques for bisimulation verification

Abstract

We advocate the use of the up—to techniques for bisimulation in the field of automatic verification. To this end, we develop a tool to perform proofs using the up to structural congruence, the up to restrictions and the up to parallel composition proof techniques for bisimulation between π—calculus terms. The latter technique is of particular interest because it allows one to reason on infinite state space processes. To use it in full effect, we adapt the “on the fly” bisimulation checking algorithm, leading to a form of computational completeness. The usefulness of these techniques in dealing with the expressive power of the π—calculus is illustrated on two non trivial examples, namely the treatment of persistent data structures and the alternating bit protocol. These examples are also good opportunities to study how well—known π—calculus encodings behave in the framework of automatic verification.