Paper Info
Title
A Nested Depth First Search Algorithm for Model Checking with Symmetry Reduction
Abstract
We present an algorithm for the verification of properties of distributed systems, represented as B眉chi automata, which exploits symmetry reduction. The algorithm is developed in the more general context of bisimulation preserving reductions along the lines of Emerson, Jha and Peled. Our algorithm is a modification of the nested depth first search (NDFS) algorithm by Courcoubetis, Yannakakis, Vardi and Wolper. As such, it has the standard advantages (memory and time efficiency) that NDFS shows over the state space exploration algorithms based on maximal strongly connected components in the state space graph. In addition, a nice feature of the presented algorithm is that it works also with multiple (non-canonical) representatives for the symmetry equivalence classes. Also, instead of an abstract counter-example, our algorithm is capable of reproducing a counter-example which exists in the original unreduced state space, which is an important feature for debugging.
Year
DOI
Venue
2002
10.1007/3-540-36135-9_5
formal techniques for (networked and) distributed systems
Keywords
DocType
Volume
important feature,nice feature,abstract counter-example,symmetry equivalence class,state space exploration,model checking,original unreduced state space,state space graph,chi automaton,nested depth first search,symmetry reduction,general context,distributed system,bisimulation
Conference
2529
ISSN
ISBN
Citations 
0302-9743
3-540-00141-7
2
PageRank 
References 
Authors
0.38
12
1
Name
Order
Citations
PageRank
Dragan Bosnacki127626.95