ARC - A tool for efficient refinement and equivalence checking for CSP

This paper presents the design and implementation of ARC - a tool for automated verification of concurrent systems. The tool is based on the untimed CSP language, its semantic models and theory of refinement. We alleviate the combinatorial explosion problem using Ordered Binary Decision Diagrams (OBDDs) for the internal representation of complex data structures - sets and labeled transition systems (LTS). The semantically complex external choice operator is translated into the corresponding LTS using an optimized algorithm. This and some other implementation improvements allow verifying systems with up to 10(33) states, which is consistent with the capabilities of other OBDD-based approaches. Compared to two existing CSP tools, FDR and MRC, ARC has fewer language restrictions and is more memory efficient. A performance comparison based on the n-schedulers and dining philosophers problems suggests that the checking algorithm of ARC is, in most cases, taster than those of the other tools.