Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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)
Bošnački, D., Dams, D., Holenderski, L.: Symmetric Spin. International Journal on Software Tools for Technology Transfer 4(1), 65–80 (2002)
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)
Clarke, Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press (2000)
Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Formal Models and Semantics, pp. 995–1072. Elsevier (1990)
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)
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)
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)
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)
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)
Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996)
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 1999
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)
Holzmann, G.J.: The SPIN Model Checker - primer and reference manual. Addison-Wesley (2004)
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)
Bošnački, D., Leue, S., Lluch-Lafuente, A.: Partial-Order Reduction for General State Exploring Algorithms. STTT 11(1), 39–51 (2009)
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)
Holzmann, G., Peled, D.: An improvement in formal verification. In: FORTE 1994. Bern, Switzerland (1994)
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)
Ip, C.N., Dill, D.L.: Better verification through symmetry. Formal Methods in System Design 9, 41–75 (1996)
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)
Peled, D.: Personal communication (2001)
Valmari, A.: The state explosion problem. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 429–528. Springer, Heidelberg (1998)
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)
Valmari, A.: A Stubborn Attack on State Explosion. Formal Methods in System Design 1, 297–322 (1992)
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)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Bošnački, D., Scheffer, M. (2015). Partial Order Reduction and Symmetry with Multiple Representatives. In: Havelund, K., Holzmann, G., Joshi, R. (eds) NASA Formal Methods. NFM 2015. Lecture Notes in Computer Science(), vol 9058. Springer, Cham. https://doi.org/10.1007/978-3-319-17524-9_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-17524-9_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-17523-2
Online ISBN: 978-3-319-17524-9
eBook Packages: Computer ScienceComputer Science (R0)