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. Processesmay communicate via broadcast, rendez-vous and shared variables. The method derives an over-approximation of the induced transitionsystem, which allows the use of a simple class of regular expressions as a symbolic representation. Compared to traditionalregular model checking methods, the analysis does not require the manipulation of transducers, and hence its simplicity andefficiency. We have implemented a prototype which works well on several mutual exclusion algorithms and cache coherence protocols.
%0 Journal Article
%1 parosh2007regular
%A Abdulla, Parosh
%A Delzanno, Giorgio
%A Henda, Noomene
%A Rezine, Ahmed
%D 2007
%J Tools and Algorithms for the Construction and Analysis of Systems
%K modelchecking regular
%P 721--736
%T Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems)
%U http://dx.doi.org/10.1007/978-3-540-71209-1_56
%X 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. Processesmay communicate via broadcast, rendez-vous and shared variables. The method derives an over-approximation of the induced transitionsystem, which allows the use of a simple class of regular expressions as a symbolic representation. Compared to traditionalregular model checking methods, the analysis does not require the manipulation of transducers, and hence its simplicity andefficiency. We have implemented a prototype which works well on several mutual exclusion algorithms and cache coherence protocols.
@article{parosh2007regular,
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. Processesmay communicate via broadcast, rendez-vous and shared variables. The method derives an over-approximation of the induced transitionsystem, which allows the use of a simple class of regular expressions as a symbolic representation. Compared to traditionalregular model checking methods, the analysis does not require the manipulation of transducers, and hence its simplicity andefficiency. We have implemented a prototype which works well on several mutual exclusion algorithms and cache coherence protocols.},
added-at = {2010-01-06T17:32:50.000+0100},
author = {Abdulla, Parosh and Delzanno, Giorgio and Henda, Noomene and Rezine, Ahmed},
biburl = {https://www.bibsonomy.org/bibtex/2364f5196b2d4150f4affc67899473c84/giuliano.losa},
description = {Regular Model Checking Without Transducers},
interhash = {864ae03139680b9a9d064904fda786bf},
intrahash = {364f5196b2d4150f4affc67899473c84},
journal = {Tools and Algorithms for the Construction and Analysis of Systems},
keywords = {modelchecking regular},
pages = {721--736},
timestamp = {2010-01-06T17:32:50.000+0100},
title = {Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems)},
url = {http://dx.doi.org/10.1007/978-3-540-71209-1_56},
year = 2007
}