Safety Property-Driven Stubborn Sets

  • Henri HansenEmail author
  • Antti Valmari
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9899)


A new reduced state space construction method is presented where in every constructed state, the set of transitions that are fired is chosen based on the safety property that is being verified. Typical earlier methods only take the property into account in one state of each cycle or in one state of each terminal strong component of the reduced state space. They may fire totally irrelevant transitions in the other states. Where the property is taken into account, typically many or all enabled transitions are fired. This has spoiled attempts to be property-driven in every state. The present study exploits an idea that was published in 2016 with which this can be avoided. Furthermore, most earlier methods classify the transitions to visible and invisible. The new method uses a novel improved concept. An experiment is presented where the new concept provides significant improvement to the reduction results.


Model Check Data Packet Visibility Condition Safety Property Visible Transition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Evangelista, S., Pajault, C.: Solving the ignoring problem for partial order reduction. Int. J. Softw. Tools Technol. Transf. 12(2), 155–170 (2010)CrossRefGoogle Scholar
  2. 2.
    Eve, J., Kurki-Suonio, R.: On computing the transitive closure of a relation. Acta Informatica 8(4), 303–314 (1977)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Hansen, H., Wang, X.: Compositional analysis for weak stubborn sets. In: 11th International Conference on Application of Concurrency to System Design (ACSD), pp. 36–43. IEEE (2011)Google Scholar
  4. 4.
    Latvala, T.: Efficient model checking of safety properties. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 74–88. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  5. 5.
    Peled, D., Valmari, A., Kokkarinen, I.: Relaxed visibility enhances partial order reduction. Formal Methods Syst. Des. 19(3), 275–289 (2001)CrossRefzbMATHGoogle Scholar
  6. 6.
    Tarjan, R.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146–160 (1972)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Valmari, A.: On-the-fly verification with stubborn sets. In: Courcoubetis, C. (ed.) Computer Aided Verification, vol. 697, pp. 397–408. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  8. 8.
    Valmari, A.: A state space tool for concurrent system models expressed in C++. In: SPLST 2015. CEUR Workshop Proceedings, vol. 1525, pp. 377–397 (2015)Google Scholar
  9. 9.
    Valmari, A.: Stop it, and be stubborn! In: 15th International Conference on Application of Concurrency to System Design (ACSD), pp. 10–19. IEEE (2015)Google Scholar
  10. 10.
    Valmari, A., Hansen, H.: Stubborn set intuition explained. In: Cabac, L., Kristensen, L.M., Rölke, H. (eds.) Proceedings of the International Workshop on Petri Nets and Software Engineering, PNSE 2016, CEUR Workshop Proceedings, vol. 1591, Toruń, Poland, 20–21 June 2016, pp. 213–232. (2016).
  11. 11.
    Valmari, A., Vogler, W.: Fair testing and stubborn sets. In: Bošnacki, D., Wijs, A. (eds.) SPIN 2016. LNCS, vol. 9641, pp. 225–243. Springer, Heidelberg (2016). doi: 10.1007/978-3-319-32582-8_16 CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.Department of MathematicsTampere University of TechnologyTampereFinland

Personalised recommendations