Abstract
Partial order reduction covers a range of techniques based on eliminating unnecessary transitions when generating a state space. On the other hand, abstractions replace sets of states of a system with abstract representatives in order to create a smaller state space. This article explores how stubborn sets and abstraction can be combined. We provide examples to provide intuition and expand on some recent results. We provide a classification of abstractions and give some novel results on what is needed to combine abstraction and partial order reduction in a sound way.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Bošnački, D., Scheffer, M.: Partial order reduction and symmetry with multiple representatives. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 97–111. Springer, Heidelberg (2015). doi:10.1007/978-3-319-17524-9_8
Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000). doi:10.1007/10722167_15
Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Programm. Lang. Syst. (TOPLAS) 16(5), 1512–1542 (1994)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT press, Cambridge (1999)
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). doi:10.1007/3-540-56922-7_38
Engelfriet, J.: Determinancy \(\rightarrow \) (observation equivalence = trace equivalence). Theor. Comput. Sci. 36, 21–25 (1985)
Geldenhuys, J., Hansen, H., Valmari, A.: Exploring the scope for partial order reduction. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 39–53. Springer, Heidelberg (2009). doi:10.1007/978-3-642-04761-9_4
Gibson-Robinson, T., Hansen, H., Roscoe, A.W., Wang, X.: Practical partial order reduction for CSP. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 188–203. Springer, Heidelberg (2015). doi:10.1007/978-3-319-17524-9_14
Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996). doi:10.1007/3-540-60761-7
Hansen, H., Kwiatkowska, M., Qu, H.: Partial order reduction for model checking Markov decision processes under unconditional fairness. In: Quantitative Evaluation of Systems (QEST 2011), pp. 203–212. IEEE (2011)
Hansen, H., Lin, S.-W., Liu, Y., Nguyen, T.K., Sun, J.: Diamonds are a girl’s best friend: partial order reduction for timed automata with abstractions. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 391–406. Springer, Heidelberg (2014). doi:10.1007/978-3-319-08867-9_26
Hansen, H., Valmari, A.: Operational determinism and fast algorithms. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 188–202. Springer, Heidelberg (2006). doi:10.1007/11817949_13
Hansen, H., Valmari, A.: Safety property-driven stubborn sets. In: Larsen, K.G., Potapov, I., Srba, J. (eds.) RP 2016. LNCS, vol. 9899, pp. 90–103. Springer, Heidelberg (2016). doi:10.1007/978-3-319-45994-3_7
Hansen, H., Wang, X.: Compositional analysis for weak stubborn sets. In: 2011 11th International Conference on Application of Concurrency to System Design (ACSD), pp. 36–43. IEEE (2011)
Laarman, A., Pater, E., van de Pol, J., Hansen, H.: Guard-based partial-order reduction. Int. J. Softw. Tools Technol. Transfer 18(4), 427–448 (2016)
Milner, R. (ed.): A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980). doi:10.1007/3-540-10235-3
Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993). doi:10.1007/3-540-56922-7_34
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Upper Saddle River (1997)
Valmari, A.: A stubborn attack on state explosion. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 156–165. Springer, Heidelberg (1991). doi:10.1007/BFb0023729
Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) ICATPN 1989. LNCS, vol. 483, pp. 491–515. Springer, Heidelberg (1991). doi:10.1007/3-540-53863-1_36
Valmari, A.: Stubborn set methods for process algebras. In: Proceedings of the DIMACS Workshop on Partial Order Methods in Verification (1997)
Valmari, A., Hansen, H.: Can stubborn sets be optimal? Fundamenta Informaticae 113(3–4), 377–397 (2011)
Valmari, A., Hansen, H.: Stubborn set intuition explained. In: International Workshop on Petri Nets and Software Engineering 2016, pp. 213–232 (2016)
Valmari, A., Tienari, M.: Compositional failure-based semantic models for basic lotos. Formal Aspects Comput. 7(4), 440–468 (1995)
Valmari, A., Vogler, W.: Fair testing and stubborn sets. In: Bošnački, D., Wijs, A. (eds.) SPIN 2016. LNCS, vol. 9641, pp. 225–243. Springer, Heidelberg (2016). doi:10.1007/978-3-319-32582-8_16
Glabbeek, R.J.: The linear time — branching time spectrum II. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 66–81. Springer, Heidelberg (1993). doi:10.1007/3-540-57208-2_6
Acknowledgements
I wish to thank the editors for inviting me to submit an article, Antti Valmari for pioneering the field and his eagerness to discuss the topic after all these years, Xu Wang for discussions we have had over the years about the merits and pitfalls of various approaches, and Dragan Bosnacki for providing some insights on the matter. I am grateful to Bill Roscoe, for asking me one instrumental question about partial order reduction years ago. Answering that question led me to write a few articles, and, in a way, also this one.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this chapter
Cite this chapter
Hansen, H. (2017). Abstractions for Transition Systems with Applications to Stubborn Sets. In: Gibson-Robinson, T., Hopcroft, P., Lazić, R. (eds) Concurrency, Security, and Puzzles. Lecture Notes in Computer Science(), vol 10160. Springer, Cham. https://doi.org/10.1007/978-3-319-51046-0_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-51046-0_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-51045-3
Online ISBN: 978-3-319-51046-0
eBook Packages: Computer ScienceComputer Science (R0)