Abstract
An important component of partial-order based reduction algorithms is the condition that prevents action ignoring, commonly known as the cycle proviso. In this paper we give a new version of this proviso that is applicable to a general search algorithm skeleton also known as the General State Expanding Algorithm (GSEA). GSEA maintains a set of open (visited but not expanded) states from which states are iteratively selected for exploration and moved to a closed set of states (visited and expanded). Depending on the open set data structure used, GSEA can be instantiated as depth-first, breadth-first, or a directed search algorithm. The proviso is characterized by reference to the open and closed set of states in GSEA. As a result the proviso can be computed in an efficient manner during the search based on local information. We implemented partial-order reduction for GSEA based on our proposed proviso in the tool HSF-SPIN, which is an extension of the model checker SPIN for directed model checking. We evaluate the state space reduction achieved by partial-order reduction according to the proviso that we propose by comparing it on a set of benchmark problems to other reduction approaches. We also compare the use of breadth-first search and A*, two algorithms ensuring that counterexamples of minimal length will be found, together with the proviso that we propose.
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.: Partialorder reduction in symbolic state-space exploration. Formal Methods in System Design 18, 97–116 (2001); Grumberg, O. (ed.): CAV 1997. LNCS, vol. 1254, pp. 97–116. Springer, Heidelberg (1997)
Bošnački, D., Holzmann, G.J.: Improving Spin’s Partial-Order Reduction for Breadth-First Search. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 91–105. Springer, Heidelberg (2005)
Bošnački, D., Leue, S., Lluch Lafuente, A.: Partial-Order Reduction for General State Exploring Algorithms, Technical Report soft-05-02, Chair for Software Engineering, University of Konstanz (2005), http://www.inf.uni-konstanz.de/soft/research/publications/pdf/soft-05-01.pdf
Clarke, E., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)
Edelkamp, S., Lluch Lafuente, A., Leue, S.: Directed explicit-state model checking in the validation of communication protocols. Software Tools for Technology Transfer 5, 247–267 (2004)
Edelkamp, S., Leue, S., Lluch Lafuente, A.: Partial-order reduction and trail improvement in directed model checking. International Journal on Software Tools for Technology Transfer 6(4), 277–301 (2004)
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)
Hart, P.E., Nilsson, N.J., Raphael, B.: A formal basis for heuristic determination of minimum path costs. IEEE Transactions on Systems Science and Cybernetics 4, 100–107 (1968)
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.J., Peled, D.: An Improvement in Formal Verification, FORTE 1994, Bern, Switzerland (1994)
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.: Directed Search for the Verification of Communication Protocols, PhD Thesis, Freiburger Dokument Server, Institute of Computer Science, University of Freiburg (June 2003)
Levin, V., Palmer, R., Qadeer, S., Rajamani, S.K.: Sound Transaction-Based Reduction Without Cycle Detection. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 106–121. Springer, Heidelberg (2005)
Nalumasu, R., Gopalakrishnan, G.: An Efficient Partial-Order Reduction Algorithm with an Alternative Proviso Implementation. Formal Methods in System Design 20(3), 231–247 (2002)
Nilsson, N.J.: Principles of Artificial Intelligence. Tioga Publishing Co. Palo Alto, California (1980)
Overman, W.T.: Verification of Concurrent Systems: Function and Timing, Ph.D. Thesis, UCLA, Los Angeles, California (1981)
Palmer, R., Gopalakrishnan, G.: A Distributed Partial Order Reduction Algorithm. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, p. 370. Springer, Heidelberg (2002)
Pearl, J.: Heuristics. Addison-Wesley, Reading (1985)
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. LCNS, vol. 818, pp. 377–390, (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, New Brunswick. LICS, vol. 96, 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: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. 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
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bošnački, D., Leue, S., Lafuente, A.L. (2006). Partial-Order Reduction for General State Exploring Algorithms. In: Valmari, A. (eds) Model Checking Software. SPIN 2006. Lecture Notes in Computer Science, vol 3925. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11691617_16
Download citation
DOI: https://doi.org/10.1007/11691617_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33102-5
Online ISBN: 978-3-540-33103-2
eBook Packages: Computer ScienceComputer Science (R0)