Distributed On-the-Fly Equivalence Checking

Christophe Joubert and Radu Mateescu


Abstract

On-the-fly equivalence checking consists in comparing two Labeled Transition Systems (LTSs) modulo an equivalence relation by exploring them in a demand-driven way, which allows to detect errors in LTSs too large to be constructed explicitly. In this paper, we aim at further improving the performance of on-the-fly equivalence checking using several machines connected by a network. We propose DSOLVE, a new algorithm for distributed on-the-fly resolution of Boolean Equation Systems (BESs), which enables equivalence checking modulo various relations characterized in terms of BESs. DSOLVE serves as verification engine for the distributed version of BISIMULATOR, an on-the-fly equivalence checker developed within the CADP verification toolbox using the OPEN/CAESAR environment. Our experimental measures show quasi-linear speedups and a good scalability of the distributed version of BISIMULATOR w.r.t. its sequential version.