Can Stubborn Sets Be Optimal?

• Autorzy: Valmari A. , Hansen H.
• Języki publikacji: EN

Abstrakty

EN

Literature on the stubborn set and similar state space reduction methods presents numerous seemingly ad-hoc conditions for selecting the transitions that are investigated in the current state. There are good reasons to believe that the choice between them has a significant effect on reduction results, but not much has been published on this topic. This article presents theoretical results and examples that aim at shedding light on the issue. Because the topic is extensive, we only consider the detection of deadlocks. We distinguish between different places where choices can be made and investigate their effects. It is usually impractical to aim at choices that are "best" in some sense. However, one non-trivial practical optimality result is proven.

Słowa kluczowe

EN

Petri net; COncurrent SYstem; state spaces

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2011
• Tom: Vol. 113, nr 3/4
• Strony: 377--397
• Opis fizyczny: Bibliogr. 15 poz., wykr.

Twórcy

autor

Valmari A.

autor

Hansen H.

• Tampere University of Technology, Department of Software Systems, PO Box 553, FI-33101 Tampere, Finland,

Bibliografia

• [1] Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
• [2] Esparza, J.: Decidability and Complexity of Petri Net Problems - An Introduction. In: Reisig,W., Rozenberg, G. (eds.) Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, LNCS, vol. 1491, pp. 374-428. Springer, Heidelberg (1998)
• [3] Flanagan, C., Godefroid, P.: Dynamic Partial-Order Reduction for Model Checking Software. In: Proceedings of the 32nd Annual ACM Symposium on Principles of Programming Languages, pp. 110-121 (2005)
• [4] Geldenhuys, J., Hansen, H., Valmari, A.: Exploring the Scope for Partial Order Reduction. In: Liu, Z., Ravn, A.P. (eds.) Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009. LNCS, vol. 5799, pp. 39-53. Springer, Heidelberg (2009)
• [5] Godefroid, P.: Using Partial Orders to Improve Automatic Verification Methods. In: Proceedings of CAV'90, AMS-ACM DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 3, pp. 321-340 (1991)
• [6] Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. LNCS, vol. 1032. Springer, Heidelberg (1996)
• [7] Groote, J.F., Sellink,M.P.A.: Confluence for Process Verification, Theoretical Computer Science, vol. 170(1-2), pp. 47-81 (1996)
• [8] Hansen, H., Wang, Xu: Compositional Analysis for Weak Stubborn Sets. In: Caillaud, B., Carmona, J., Hiraishi, K. (eds.) Application of Concurrency to System Design, 11th International Conference, ACSD 2011. pp. 36-43. IEEE CS Press (2011)
• [9] Peled, D.: All from One, One for All: On Model Checking Using Representatives. In: Courcoubetis, C. (ed.) Computer Aided Verification, 5th International Conference, CAV 1993. LNCS, vol. 697, pp. 409-423. Springer, Heidelberg (1993)
• [10] Peled, D., Valmari, A., Kokkarinen, I.: Relaxed Visibility Enhances Partial Order Reduction. Formal Methods in System Design 19, 275-289 (2001)
• [11] Rauhamaa, M.: A Comparative Study of Methods for Efficient Reachability Analysis. Lic. Tech. Thesis, Helsinki University of Technology, Digital Systems Laboratory, Research Report A-14. Espoo, Finland (1990)
• [12] 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)
• [13] Valmari, A.: The State Explosion Problem. In: Reisig, W., Rozenberg, G. (eds.) Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, LNCS, vol. 1491, pp. 429-528. Springer, Heidelberg (1998)
• [14] Valmari, A., Hansen, H.: Can Stubborn Sets Be Optimal? In: Lilius, J., Penczek, W. (eds.): Applications and Theory of Petri Nets, 31st International Conference. LNCS, vol. 6128, pp. 43-62. Springer, Heidelberg (2010)
• [15] Varpaaniemi, K.: On the Stubborn Set Method in Reduced State Space Generation. PhD Thesis, Helsinki University of Technology, Digital Systems Laboratory Research Report A-51. Espoo, Finland (1998)