%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 }