Regular Model Checking without Transducers (On Efficient Verification of Parameterized Systems)

Parosh Aziz Abdulla, Noomene Ben Henda, Giorgio Delzanno, and Ahmed Rezine

December 2006

Abstract:

We give a simple and efficient method to prove safety properties for parameterized systems with linear topologies. A process in the system is a finite-state automaton, where the transitions are guarded by both local and global conditions. Processes may communicate via broadcast, rendez-vous and shared variables. The method derives an over-approximation of the induced transition system, which allows the use of a simple class of regular expressions as a symbolic representation. Compared to traditional regular model checking methods, the analysis does not require the manipulation of transducers, and hence its simplicity and efficiency. We have implemented a prototype which works well on several mutual exclusion algorithms and cache coherence protocols.

Note: To appear in the proceedings of TACAS 2007

Available as compressed Postscript (448 kB, no cover) and Postscript (970 kB, no cover)

Download BibTeX entry.