Abstract
We describe an improvement of the partial-order reduction algorithm for breadth-first search which was introduced in Spin version 4.0. Our improvement is based on the algorithm by Alur et al. for symbolic state model checking for local safety properties [1]. The crux of the improvement is an optimization in the context of explicit state model checking of the condition that prevents action ignoring, also known as the cycle proviso. There is an interesting duality between the cycle provisos for the breadth-first search (BFS) and depth first search (DFS) exploration of the state space, which is reflected in the role of the BFS queue and the DFS stack, respectively. The improved version of the algorithm is supported in the current version of Spin and can be shown to perform significantly better than the initial version.
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.
Similar content being viewed by others
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)
Clarke, E., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)
Gerth, R., Kuiper, R., Peled, D., Penczek, W.: A Partial Order Approach to Branching Time Logic Model Checking. Information and Computation 150(2), 132–152 (1999)
Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996)
Godefroid, P., Wolper, P.: Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 332–342. Springer, Heidelberg (1992)
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)
Holzmann, G.J., Godefroid, P., Pirottin, D.: Coverage Preserving Reduction Strategies for Reachability Analysis. In: Proc. 12th IFIP WG 6.1. International Symposium on Protocol Specification, Testing, and Validation, FORTE/PSTV 1992, pp. 349–363. North-Holland, Amsterdam (1992)
Holzmann, G., Peled, D.: An Improvement in Formal Verification. In: FORTE 1994, Bern, Switzerland (1994)
Holzmann, G., Peled, D., Yannakakis, M.: On Nested Depth First Search. In: Proc. of the 2nd Spin Workshop. Rutgers University, New Jersay (1996)
Katz, S., Peled, D.: Verification of Distributed Programs Using Representative Interleaving Sequences. Distributed Computing 6, 107–120 (1992)
Kurshan, R.P., Levin, V., Minea, M., Peled, D., Yenigün, H.: Static Partial Order Reduction. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 345–357. Springer, Heidelberg (1998)
Lluch-Lafuente, A., Edelkamp, S., Leue, S.: Partial Order Reduction in Directed Model Checking. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 112–127. Springer, Heidelberg (2002)
Overman, W.T.: Verification of Concurrent Systems: Function and Timing, Ph.D. Thesis, UCLA, Los Angeles, California (1981)
Peled, D.A.: Combining Partial Order Reductions with On-the-Fly Model Checking. Formal Methods on Systems Design 8, 39–64 (1996); A previous version appeared in Computer Aided Verification 1994. LNCS, vol. 818, pp. 377–390. Springer, Heidelberg (1994)
Willems, B., Wolper, P.: Partial Order Models for Model Checking: From Linear to Branching Time. In: Proc. of 11 Symposium of Logics in Computer Science, LICS 1996, New Brunswick, pp. 294–303 (1996)
Valmari, A.: Eliminating Redundant Interleavings during Concurrent Program Verification. In: Odijk, E., Rem, M., Syre, J.-C. (eds.) PARLE 1989. LNCS, vol. 366, pp. 89–103. Springer, Heidelberg (1989)
Valmari, A.: A Stubborn Attack on State Explosion. In: Advances in Petri Nets. LNCS, vol. 531, pp. 156–165. Springer, Heidelberg (1991)
Valmari, A.: The State Explosion Problem. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 429–528. Springer, Heidelberg (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bošnački, D., Holzmann, G.J. (2005). Improving Spin’s Partial-Order Reduction for Breadth-First Search. In: Godefroid, P. (eds) Model Checking Software. SPIN 2005. Lecture Notes in Computer Science, vol 3639. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11537328_10
Download citation
DOI: https://doi.org/10.1007/11537328_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28195-5
Online ISBN: 978-3-540-31899-6
eBook Packages: Computer ScienceComputer Science (R0)