A Prover for the muCRL toolset with applications -- version 0.1
Jaco van de Pol · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 2001
This document describes an automated theorem prover, based on an extension of binary decision diagrams. The prover transforms quantifier-free formulae into equivalent BDD-forms, w.r.t.~to some algebraic data specification. The prover is used by four tools for the symbolic analysis of distributed systems specified in $mu$CRL (i.e.~process algebra plus algebraic data types). The main techniques are invariants and confluence. Two case studies are reported: the DKR leader election protocol [13], and SPLICE [15], a coordination architecture of industrial origin. In both cases using confluence information leads to a reduced state space.