TY - GEN
T1 - A nested depth first search algorithm for model checking with symmetry reduction
AU - Bosnacki, D.
PY - 2002
Y1 - 2002
N2 - 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.
AB - 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.
U2 - 10.1007/3-540-36135-9_5
DO - 10.1007/3-540-36135-9_5
M3 - Conference contribution
SN - 3-540-00141-7
T3 - Lecture Notes in Computer Science
SP - 65
EP - 80
BT - Formal Techniques for Networked and Distributed Systems (Proceedings 22nd IFIP WG6.1 International Conference, FORTE 2002, Houston TX, USA, November 11-14, 2002)
A2 - Peled, D.A.
A2 - Vardi, M.Y.
PB - Springer
CY - Berlin
T2 - 22nd IFIP WG 6.1 International Conference Formal Techniques for Networked and Distributed Systems (FORTE 2002), November 11-14, 2002, Houston, TX, USA
Y2 - 11 November 2002 through 14 November 2002
ER -