# 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.

## Keywords

Model checking state space reduction techniques symmetry reduction nested depth first search algorithm multiple representatives## References

- 1.A.V. Aho, J.E. Hopcroft, J.D. Ulmann,
*The Design and Analysis of Computer Algorithms*, Addison Wesley, 1974.Google Scholar - 2.D. Bošnački,
*Partial Order and Symmetry Reductions for Discrete Time*, to appear in Proc. of RT-TOOLS’ 02, Copenhagen, Denmark, 2002.Google Scholar - 3.D. Bošnački, D. Dams, L. Holenderski,
*Symmetric Spin*, 7th Int. SPIN Workshop on Model Checking of Software SPIN 2000, pp. 1–19, LNCS 1885, Springer, 2000.Google Scholar - 4.E.M. Clarke, R. Enders, T. Filkorn, S. Jha, Exploiting Symmetry in Temporal Logic Model Checking,
*Formal Methods in System Design*, Vol. 19, 77–104, 1996.CrossRefGoogle Scholar - 5.E.M. Clarke, Jr., O. Grumberg, D.A. Peled,
*Model Checking*, The MIT Press, 2000.Google Scholar - 6.C. Courcoubetis, M. Vardi, P. Wolper, M. Yannakakis,
*Memory Efficient Algorithms for the Verification of Temporal Properties*, Formal Methods in System Design I, pp. 275–288, 1992.CrossRefGoogle Scholar - 7.E.A. Emerson,
*Temporal and Modal Logic*, in J. van Leeuwen (ed.), Formal Models and Semantics, pp. 995–1072, Elsevier, 1990.Google Scholar - 8.E.A. Emerson, A.P. Sistla,
*Symmetry and model checking*, Proc. of CAV’93 (Computer Aided Verification), LNCS 697, pp. 463–478, Springer, 1993.Google Scholar - 9.E.A. Emerson, A.P. Sistla,
*Utilizing Symmetry when Model Checking under Fairness Assumptions: An Automata-theoretic Approach*, ACM Transactions on Programming Languages and Systems, Vol. 19, 4, pp. 617–638, ACM Press, 1997.CrossRefGoogle Scholar - 10.E.A. Emerson, S. Jha, D. Peled,
*Combining partial order and symmetry reductions*, in Ed Brinksma (ed.), Proc. of TACAS’97 (Tools and Algorithms for the Construction and Analysis of Systems), LNCS 1217, pp. 19–34, Springer, 1997.Google Scholar - 11.V. Gyuris, A.P. Sistla,
*On-the fly model checking under fairness that exploits symmetry*, in O. Grumberg (ed.), Proc. of CAV’97 (Computer Aided Verification), LNCS 1254, pp. 232–243, Springer, 1997.Google Scholar - 12.G.J. Holzmann,
*Design and Validation of Communication Protocols*, Prentice Hall, 1991. Also: http://netlib.bell-labs.com/netlib/spin/whatispin.html. - 13.G. Holzmann, D. Peled, M. Yannakakis,
*On Nested Depth First Search*, Proc. of the 2nd Spin Workshop, Rutgers University, New Jersey, USA, 1996.Google Scholar - 14.R. Iosif,
*Symmetry Reduction Criteria for Software Model Checking*, Model Checking Software, Proc. of SPIN 2002, LNCS 2318, pp. 22–41, Springer, 2002.Google Scholar - 15.C.N. Ip, D.L. Dill, Better verification through symmetry.
*Formal Methods in System Design*, Vol. 9, pp. 41–75, 1996.CrossRefGoogle Scholar - 16.W. Thomas, Automata on Infinite Objects, in J. van Leeuwen (ed.), Formal Models and Semantics, pp. 995–1072 Elsevier, 1990.Google Scholar
- 17.M. Vardi, P. Wolper,
*An automata-theoretic approach to automatic program verification*. In Proc. of the 1st Symposium on Logic in Computer Science LICS’ 86, pp. 322–331, 1986.Google Scholar - 18.P. Wolper, D. Leroy,
*Reliable Hashing without Collision Detection*, Proc. of CAV’93 (Computer Aided Verification), LNCS 697, pp. 59–70, Springer, 1993.Google Scholar