On automating process algebra proofs

Abstract

In [10] Groote and Springintveld incorporated several model-oriented techniques - such as invariants, matching criteria, state mappings - in the process-algebraic framework of μCRL for structuring and simplifying protocol verifications. In this paper, we formalise these extensions in Coq, which is a proof development tool based on type theory. In the updated framework, the length of proof constructions is reduced significantly. Moreover, the new approach allows for more automation (proof generation) than was possible in the past. The results are illustrated by an example in which we prove two queue representations equal.