Top

Published in:

2017 | OriginalPaper | Chapter

Stubborn Set Intuition Explained

Authors : Antti Valmari, Henri Hansen

Published in: Transactions on Petri Nets and Other Models of Concurrency XII

Publisher: Springer Berlin Heidelberg

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

This study focuses on the differences between stubborn sets and other partial order methods. First a major problem with step graphs is pointed out with an example. Then the deadlock-preserving stubborn set method is compared to the deadlock-preserving ample set and persistent set methods. Next, conditions are discussed whose purpose is to ensure that the reduced state space preserves the ordering of visible transitions, that is, transitions that may change the truth values of the propositions that the formula under verification has been built from. Finally solutions to the ignoring problem are analysed both when the purpose is to preserve only safety properties and when also liveness properties are of interest.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Transition Systems Reduction: Balancing Between Precision and Simplicity

next chapter Decomposed Replay Using Hiding and Reduction as Abstraction

Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999). 314 p

Evangelista, S., Pajault, C.: Solving the ignoring problem for partial order reduction. Software Tools Technol. Transf. 12(2), 155–170 (2010)CrossRef

Eve, J., Kurki-Suonio, R.: On computing the transitive closure of a relation. Acta Informatica 8(4), 303–314 (1977)MathSciNetCrossRefMATH

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, Cham (2015). doi:10.1007/978-3-319-17524-9_14

Godefroid, P.: Using partial orders to improve automatic verification methods. In: Clarke, E.M., Kurshan, R.P. (eds.) Computer-Aided Verification 1990, AMS-ACM DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 3, pp. 321–340 (1991)

Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996)MATH

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, Cham (2014). doi:10.1007/978-3-319-08867-9_26

Laarman, A., Pater, E., van de Pol, J., Weber, M.: Guard-based partial-order reduction. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 227–245. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39176-7_15 CrossRef

Mazurkiewicz, A.: Trace theory. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) ACPN 1986. LNCS, vol. 255, pp. 278–324. Springer, Heidelberg (1987). doi:10.1007/3-540-17906-2_30 CrossRef

10.

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 CrossRef

11.

Peled, D.: Ten years of partial order reduction. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 17–28. Springer, Heidelberg (1998). doi:10.1007/BFb0028727 CrossRef

12.

Rauhamaa, M.: A comparative study of methods for efficient reachability analysis. Lic. Technical Thesis, Helsinki University of Technology, Digital Systems Laboratory, Research Report A-14. Espoo, Finland (1990)

13.

Roscoe, A.W.: Understanding Concurrent Systems. Springer, Heidelberg (2010). doi:10.1007/978-1-84882-258-0. 533 p.CrossRefMATH

14.

Tarjan, R.E.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146–160 (1972)MathSciNetCrossRefMATH

15.

Valmari, A.: Error detection by reduced reachability graph generation. In: Proceedings of the 9th European Workshop on Application and Theory of Petri Nets, pp. 95–122 (1988)

16.

Valmari, A.: State Space Generation: Efficiency and Practicality. Dr. Technical Thesis, Tampere University of Technology Publications 55, Tampere (1988)

17.

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 CrossRef

18.

Valmari, A.: Stubborn set methods for process algebras. In: Peled, D., Pratt, V., Holzmann, G. (eds.) Partial Order Methods in Verification, Proceedings of a DIMACS Workshop, DIMACS Series in Discrete Mathematics and Theoretical Computer Science vol. 29, pp. 213–231. American Mathematical Society (1997)

19.

Valmari, A.: The state explosion problem. In: Reisig, W., Rozenberg, G. (eds.) ACPN 1996. LNCS, vol. 1491, pp. 429–528. Springer, Heidelberg (1998). doi:10.1007/3-540-65306-6_21 CrossRef

20.

Valmari, A.: Stop it, and be stubborn!. In: Haar, S., Meyer, R. (eds.) 15th International Conference on Application of Concurrency to System Design, pp. 10–19. IEEE Computer Society (2015)

21.

Valmari, A.: A state space tool for concurrent system models expressed in C++. In: Nummenmaa, J., Sievi-Korte, O., Mäkinen, E. (eds.) CEUR Workshop Proceedings of SPLST 2015, Symposium on Programming Languages and Software Tools, vol. 1525, pp. 91–105 (2015)

22.

Valmari, A.: Stop it, and be stubborn!. ACM Trans. Embed. Comput. Syst. 16(2), 46:1–46:26 (2017)CrossRef

23.

Valmari, A.: More stubborn set methods for process algebras. In: Gibson-Robinson, T., Hopcroft, P., Lazić, R. (eds.) Concurrency, Security, and Puzzles. LNCS, vol. 10160, pp. 246–271. Springer, Cham (2017). doi:10.1007/978-3-319-51046-0_13 CrossRef

24.

Valmari, A., Hansen, H.: Can stubborn sets be optimal? Fundam. Informaticae 113(3–4), 377–397 (2011)MathSciNetMATH

25.

Valmari, A., Hansen, H.: Stubborn set intuition explained. In: Cabac, L., Kristensen, L.M., Rölke, H. (eds.) CEUR Workshop Proceedings of the International Workshop on Petri Nets and Software Engineering 2016, vol. 1591, pp. 213–232 (2016)

26.

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, Cham (2016). doi:10.1007/978-3-319-32582-8_16 CrossRef

27.

Varpaaniemi, K.: On the Stubborn Set Method in Reduced State Space Generation. Ph.D. Thesis, Helsinki University of Technology, Digital Systems Laboratory Research Report A-51, Espoo, Finland (1998)

Title: Stubborn Set Intuition Explained
Authors: Antti Valmari
Henri Hansen
Publisher: Springer Berlin Heidelberg
Book: Transactions on Petri Nets and Other Models of Concurrency XII
Print ISBN: 978-3-662-55861-4

Electronic ISBN: 978-3-662-55862-1

Copyright Year: 2017
DOI: https://doi.org/10.1007/978-3-662-55862-1_7

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner