Abstract
We present an algorithm for partial order reduction in the context of a countable universe of deterministic actions, of which finitely many are enabled at any given state. This means that the algorithm is suited for a setting in which resources, such as processes or objects, are dynamically created and destroyed, without an a priori bound. The algorithm relies on abstract enabling and disabling relations among actions, rather than associated sets of concurrent processes. It works by selecting so-called probe sets at every state, and backtracking in case the probe is later discovered to have missed some possible continuation.
We show that this improves the potential reduction with respect to persistent sets. We then instantiate the framework by assuming that states are essentially sets of entities (out of a countable universe) and actions test, delete and create such entities. Typical examples of systems that can be captured in this way are Petri nets and (more generally) graph transformation systems. We show that all the steps of the algorithm, including the estimation of the missed actions, can be effectively implemented for this setting.
This work has been carried out in the context of the GROOVE project funded by the Dutch NWO (project number 612.000.314).
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
Diekert, V., Rozenberg, G.: The Book of Traces. World Scientific Publishing Co., Inc., Singapore (1995)
Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proc. of the 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2005), pp. 110–121. ACM Press, New York (2005)
Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. LNCS, vol. 1032. Springer, Heidelberg (1996)
Godefroid, P., Wolper, P.: Using partial orders for the efficient verification of deadlock freedom and safety properties. Formal Methods in System Design 2(2), 149–164 (1993)
Gueta, G., Flanagan, C., Yahav, E., Sagiv, M.: Cartesian partial-order reduction. In: Bosnacki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 5495, pp. 95–112. Springer, Heidelberg (2007)
Janicki, R., Koutny, M.: Structure of concurrency. Theor. Comput. Sci. 112(1), 5–52 (1993)
Kastenberg, H., Rensink, A.: Model checking dynamic states in GROOVE. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 299–305. Springer, Heidelberg (2006)
Langerak, R.: Transformations and Semantics for LOTOS. PhD thesis, University of Twente (1992)
Mazurkiewicz, A.W.: Trace theory. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol. 255, pp. 279–324. Springer, Heidelberg (1987)
Rensink, A.: The GROOVE Simulator: A tool for state space generation. In: Pfaltz, J.L., Nagl, M., Böhlen, B. (eds.) AGTIVE 2003. LNCS, vol. 3062, pp. 479–485. Springer, Heidelberg (2004)
Rensink, A.: Explicit state model checking for graph grammars. In: Degano, P., De Nicola, R., Meseguer, J. (eds.) Festschrift for Ugo Montanari. LNCS, vol. 5065. Springer, Heidelberg (2008)
Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) APN 1990. LNCS, vol. 483, pp. 491–515. Springer, Heidelberg (1991)
Valmari, A.: On-the-fly verification with stubborn sets. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 397–408. Springer, Heidelberg (1993)
Winskel, G.: Event structures. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol. 255, pp. 325–392. Springer, Heidelberg (1987)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kastenberg, H., Rensink, A. (2008). Dynamic Partial Order Reduction Using Probe Sets. In: van Breugel, F., Chechik, M. (eds) CONCUR 2008 - Concurrency Theory. CONCUR 2008. Lecture Notes in Computer Science, vol 5201. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85361-9_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-85361-9_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85360-2
Online ISBN: 978-3-540-85361-9
eBook Packages: Computer ScienceComputer Science (R0)