A nested depth first search algorithm for model checking with symmetry reduction

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

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.
Original languageEnglish
Title of host publicationFormal Techniques for Networked and Distributed Systems (Proceedings 22nd IFIP WG6.1 International Conference, FORTE 2002, Houston TX, USA, November 11-14, 2002)
EditorsD.A. Peled, M.Y. Vardi
Place of PublicationBerlin
PublisherSpringer
Pages65-80
ISBN (Print)3-540-00141-7
DOIs
Publication statusPublished - 2002
Event22nd IFIP WG 6.1 International Conference Formal Techniques for Networked and Distributed Systems (FORTE 2002), November 11-14, 2002, Houston, TX, USA - Houston, TX, United States
Duration: 11 Nov 200214 Nov 2002

Publication series

NameLecture Notes in Computer Science
Volume2529
ISSN (Print)0302-9743

Conference

Conference22nd IFIP WG 6.1 International Conference Formal Techniques for Networked and Distributed Systems (FORTE 2002), November 11-14, 2002, Houston, TX, USA
Abbreviated titleFORTE 2002
CountryUnited States
CityHouston, TX
Period11/11/0214/11/02

Fingerprint Dive into the research topics of 'A nested depth first search algorithm for model checking with symmetry reduction'. Together they form a unique fingerprint.

Cite this