Abstract
The stubborn set method is one of the methods that try to relieve the state space explosion problem that occurs in state space generation. This paper is concentrated on the verification of nexttime-less LTL (linear time temporal logic) formulas with the aid of the stubborn set method. The contribution of the paper is a theorem that gives us a way to utilize the structure of the formula when the stubborn set method is used and there is no fairness assumption. Connections to already known results are drawn by modifying the theorem to concern verification under fairness assumptions.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bause, F.: Analysis of Petri Nets with a Dynamic Priority Method. Azéma, P., and Balbo, G. (Eds.), Proceedings of PN’ 97, Toulouse. LNCS 1248, Springer-Verlag 1997, pp. 215–234.
Courcoubetis, C. (Ed.): Proceedings of CAV’ 93, Elounda, Greece. LNCS 697, Springer-Verlag 1993, 504 p.
Dembiński, P., and Średniawa, M. (Eds.): Proceedings of PSTV’ 95, Warsaw. Chapman & Hall 1996, 453 p.
Emerson, E.A.: Temporal and Modal Logic. van Leeuwen, J. (Ed.), Handbook of Theoretical Computer Science, Vol. B. Elsevier 1990, pp. 995–1072.
Francez, N.: Fairness. Springer-Verlag 1986, 295 p.
Gerth, R., Kuiper, R., Peled, D., and Penczek, W.: A Partial Order Approach to Branching Time Logic Model Checking. Proceedings of the 3rd Israel Symposium on Theory of Computing and Systems, Tel Aviv 1995. IEEE Computer Society Press, Los Alamitos CA 1995, pp. 130–140.
Gerth, R., Peled, D., Vardi, M.Y., and Wolper, P.: Simple On-the-Fly Automatic Verification of Linear Temporal Logic. In Średniawa, M. (Eds.): Proceedings of PSTV’ 95, Warsaw. Chapman & Hall 1996 [3], pp. 3–18.
Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems — An Approach to the State-Explosion Problem. LNCS 1032, Springer-Verlag 1996, 143 p.
Godefroid, P., and Pirottin, D.: Refining Dependencies Improves Partial-Order Verification Methods. In [2], pp. 438–449.
Janicki, R., and Koutny, M.: Using Optimal Simulations to Reduce Reachability Graphs. Clarke, E.M., and Kurshan, R.P. (Eds.), Proceedings of CAV’ 90, New Brunswick NJ. LNCS 531, Springer-Verlag 1991, pp. 166–175.
Kaivola, R.: Equivalence, Preorders and Compositional Verification for Linear Time Temporal Logic and Concurrent Systems. Doctoral thesis, University of Helsinki, Department of Computer Science, Report A-1996-1, 1996, 185 p.
Katz, S., and Peled, D.: Verification of Distributed Programs Using Representative Interleaving Sequences. Distributed Computing 6 (1992) 2, pp. 107–120.
Kokkarinen, I., Peled, D., and Valmari, A.: Relaxed Visibility Enhances Partial Order Reduction. Grumberg, O. (Ed.), Proceedings of CAV’ 97, Haifa. LNCS 1254, Springer-Verlag 1997, pp. 328–339.
Koutny, M., and Pietkiewicz-Koutny, M.: On the Sleep Sets Method for Partial Order Verification of Concurrent Systems. University of Newcastle upon Tyne, Department of Computing Science, Technical Report 495, Newcastle upon Tyne 1994.
Overman, W.T.: Verification of Concurrent Systems: Function and Timing. PhD thesis, University of California at Los Angeles 1981, 174 p.
Peled, D.: All from One, One for All: on Model Checking Using Representatives. In [2], pp. 409–423.
Peled, D.: Combining Partial Order Reductions with On-the-Fly Model-Checking. Formal Methods in System Design 8 (1996) 1, pp. 39–64.
Peled, D., and Penczek, W.: Using Asynchronous Büchi Automata for Efficient Automatic Verification of Concurrent Systems. In Średniawa, M. (Eds.): Proceedings of PSTV’ 95, Warsaw. Chapman & Hall 1996 [3], pp. 115–130.
Ramakrishna, Y.S., and Smolka, S.A.: Partial-Order Reduction in the Weak Modal Mu-Calculus. Mazurkiewicz, A., and Winkowski, J. (Eds.), Proceedings of CONCUR’ 97, Warsaw. LNCS 1243, Springer-Verlag 1997, pp. 5–24.
Rauhamaa, M.: A Comparative Study of Methods for Efficient Reachability Analysis. Helsinki University of Technology, Digital Systems Laboratory Report A 14, 1990, 61 p.
Reisig, W.: Petri Nets: An Introduction. EATCS Monographs on Theoretical Computer Science 4, Springer-Verlag 1985, 161 p.
Sloan, R.H., and Buy, U.: Stubborn Sets for Real-Time Petri Nets. Formal Methods in System Design 11 (1997) 1, pp. 23–40.
Valmari, A.: A Stubborn Attack on State Explosion. Formal Methods in System Design 1 (1992) 4, pp. 297–322.
Valmari, A.: Stubborn Sets of Coloured Petri Nets. Proceedings of PN’ 91, Gjern, Denmark, pp. 102–121.
Valmari, A.: Alleviating State Explosion during Verification of Behavioural Equivalence. University of Helsinki, Department of Computer Science, Report A-1992-4, 1992, 57 p.
Valmari, A.: On-the-Fly Verification with Stubborn Sets. In [2], pp. 397–408.
Varpaaniemi, K.: On Combining the Stubborn Set Method with the Sleep Set Method. Valette, R. (Ed.), Proceedings of PN’ 94, Zaragoza. LNCS 815, Springer-Verlag 1994, pp. 548–567.
Vernadat, F., Azéma, P., and Michel, F.: Covering Step Graph. Billington, J., and Reisig, W. (Eds.): Proceedings of PN’ 96, Osaka. LNCS 1091, Springer-Verlag 1996, pp. 516–535.
Yoneda, T., Shibayama, A., Schlingloff, B.-H., and Clarke, E.M.: Efficient Verification of Parallel Real-Time Systems. In [2], pp. 321–332.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Varpaaniemi, K. (1998). On Stubborn Sets in the Verification of Linear Time Temporal Properties. In: Desel, J., Silva, M. (eds) Application and Theory of Petri Nets 1998. ICATPN 1998. Lecture Notes in Computer Science, vol 1420. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-69108-1_8
Download citation
DOI: https://doi.org/10.1007/3-540-69108-1_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64677-8
Online ISBN: 978-3-540-69108-2
eBook Packages: Springer Book Archive