on-the-fly state space reductions for weak equivalences
On-the-fly verification of concurrent finite-state systems consists in constructing and analysing their underlying state spaces in a demand-driven way. This technique is able to detect errors effectively in large systems; however, its performance can still be increased by reducing the state spaces incrementally in a way compatible with the verification problem. In this paper, we propose algorithms for three on-the-fly reductions of Labeled Transition Systems (LTSs), which preserve weak equivalence relations: ?-compression (collapsing of strongly connected components made of ?-transitions), ?-closure (transitive reflexive closure over ?-transitions), and ?-confluence (a form of partial order reduction). Each algorithm is described as a reductor module taking as input the successor function of an LTS and returning the successor function of the reduced LTS. The three reductors were implemented within the CADP toolbox using the generic OPEN/CSAR environment, which makes them directly available for any on-the-fly verification tool connected to OPEN/CSAR and compatible with the underlying reduction. Our experiments show that these reductors can improve significantly the performance of on-the-fly LTS generation, model checking, and equivalence checking.
labeled transition system partial order reduction model checking equivalence checking graph exploration mu-calculus bisimulation