On-the-Fly State Space Reductions for Weak Equivalences

Radu Mateescu

Proceedings of the 10th International Workshop on Formal Methods for Industrial Critical Systems FMICS'05 (Lisbon, Portugal), September 2005

Abstract:

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: tau-compression (collapsing of strongly connected components made of tau-transitions), tau-closure (transitive reflexive closure over tau-transitions), and tau-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/CAESAR environment, which makes them directly available for any on-the-fly verification tool connected to OPEN/CAESAR 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.

10 pages

PDF

PostScript

Slides of R. Mateescu's lecture at FMICS'2005

PDF