Safety Property-Driven Stubborn Sets
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.
KeywordsModel Check Data Packet Visibility Condition Safety Property Visible Transition
- 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
- 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.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.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. CEUR-WS.org (2016). http://CEUR-WS.org/Vol-1591/