Partial Order Reduction and Symmetry with Multiple Representatives

  • Dragan BošnačkiEmail author
  • Mark Scheffer
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9058)


Symmetry reduction is one of the most successful techniques to cope with the state explosion problem in model-checking. One of the central issues in symmetry reduction is the problem of finding unique (canonical) representatives of equivalence classes of symmetric states. This problem is equivalent to the graph isomorphism problem, for which no polynomial algorithm is known. On the other hand finding multiple (non-canonical) representatives is much easier because it usually boils down to sorting algorithms. As a consequence, with multiple representatives one can significantly improve the verification times. In this paper we show that symmetry reduction with multiple representatives can be combined with partial order reduction, another efficient state space reduction technique. To this end we introduce a new weaker notion of independence which requires confluence only up to bisimulation.


Model Check Multiple Representative Atomic Proposition Label Transition System Reduction Function 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alur, R., Brayton, R.K., Henzinger, T.A., Qadeer, S., Rajamani, S.K.: Partial-Order reduction in symbolic state-space exploration. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 340–351. Springer, Heidelberg (1997) CrossRefGoogle Scholar
  2. 2.
    Bošnački, D., Dams, D., Holenderski, L.: Symmetric Spin. International Journal on Software Tools for Technology Transfer 4(1), 65–80 (2002)Google Scholar
  3. 3.
    Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting Symmetry in Temporal Logic Model Checking. Formal Methods in System Design 19, 77–104 (1996)CrossRefGoogle Scholar
  4. 4.
    Clarke, Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press (2000)Google Scholar
  5. 5.
    Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Formal Models and Semantics, pp. 995–1072. Elsevier (1990)Google Scholar
  6. 6.
    Emerson, E.A., Sistla, A.P.: Symmetry and model checking. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 463–478. Springer, Heidelberg (1993) CrossRefGoogle Scholar
  7. 7.
    Emerson, E.A., Sistla, A.P.: Utilizing symmetry when model checking under fairness assumptions: an automata theoretic approach. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 309–324. Springer, Heidelberg (1995) CrossRefGoogle Scholar
  8. 8.
    Emerson, E.A., Trefler, R.J.: From asymmetry to full symmetry: new techniques for symmetry reduction in model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 142–157. Springer, Heidelberg (1999) CrossRefGoogle Scholar
  9. 9.
    Emerson, E.A., Jha, S., Peled, D.: Combining partial order and symmetry reductions. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 19–34. Springer, Heidelberg (1997) CrossRefGoogle Scholar
  10. 10.
    Gerth, R., Kuiper, R., Peled, D., Penczek, W.: A partial order reduction approach to branching time logic model checking. In: Proc. of Third Israel Symposium on Theory on Computing and Systems, pp. 130–139, Tel Aviv, Israel. IEEE (1995)Google Scholar
  11. 11.
    Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996) zbMATHGoogle Scholar
  12. 12.
    Godefroid, P.: Exploiting symmetry when model-checking software. In: Proc. of FORTE/PSTV 1999, Formal Methods for Protocol Engineering and Distributed Systems, pp. 257–275, Beijing, October 1999Google Scholar
  13. 13.
    Gyuris, V., Sistla, A.P.: On-the fly model checking under fairness that exploits symmetry. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 232–243. Springer, Heidelberg (1997) CrossRefGoogle Scholar
  14. 14.
    Holzmann, G.J.: The SPIN Model Checker - primer and reference manual. Addison-Wesley (2004)Google Scholar
  15. 15.
    Holzmann, G.J., Bošnački, D.: The Design of a Multicore Extension of the SPIN Model Checker. IEEE Trans. Software Eng. 33(10), 659–674 (2007)Google Scholar
  16. 16.
    Bošnački, D., Leue, S., Lluch-Lafuente, A.: Partial-Order Reduction for General State Exploring Algorithms. STTT 11(1), 39–51 (2009)CrossRefGoogle Scholar
  17. 17.
    Holzmann, G.J., Godefroid, P., Pirottin, D.: Coverage preserving reduction strategies for reachability analysis, protocol specification, testing and verification, pp. 349–363, XII. Elsevier (1992)Google Scholar
  18. 18.
    Holzmann, G., Peled, D.: An improvement in formal verification. In: FORTE 1994. Bern, Switzerland (1994)Google Scholar
  19. 19.
    Iosif, R.: Symmetry reduction criteria for software model checking. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 22–41. Springer, Heidelberg (2002) CrossRefGoogle Scholar
  20. 20.
    Ip, C.N., Dill, D.L.: Better verification through symmetry. Formal Methods in System Design 9, 41–75 (1996)CrossRefGoogle Scholar
  21. 21.
    Peled, D.: Combining partial order reductions with on-the-fly model checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 377–390. Springer, Heidelberg (1994) CrossRefGoogle Scholar
  22. 22.
    Peled, D.: Personal communication (2001)Google Scholar
  23. 23.
    Valmari, A.: The state explosion problem. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 429–528. Springer, Heidelberg (1998) CrossRefGoogle Scholar
  24. 24.
    Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) Advances in Petri Nets 1990. LNCS, vol. 483, pp. 491–515. Springer, Heidelberg (1991) CrossRefGoogle Scholar
  25. 25.
    Valmari, A.: A Stubborn Attack on State Explosion. Formal Methods in System Design 1, 297–322 (1992)Google Scholar
  26. 26.
    Willems, B., Wolper, P.: Partial order models for model checking: from linear to branching time. In: Proc. of 11th Symposium of Logics in Computer Science, LICS 1996, New Brunswick, pp. 294–303 (1996)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.Eindhoven University of TechnologyEindhovenThe Netherlands

Personalised recommendations