Abstract
In the context of Petri nets, we propose an automated construction of a progress measure which is an important pre-requisite for a state space reduction technique called the sweep-line method. Our construction is based on linear-algebraic considerations concerning the transition vectors of the Petri net under consideration.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Formal Methods in System Design 9, 77–104 (1996)
Christensen, S., Kristensen, L.M., Mailund, T.: A sweep-line method for state space exploration. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 450–464. Springer, Heidelberg (2001)
Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Formal Methods in System Design 9, 105–131 (1996)
Godefroid, P., Wolper, P.: A partial approach to model checking. In: 6th IEEE Symp. on Logic in Computer Science, Amsterdam, pp. 406–415 (1991)
Huber, P., Jensen, A., Jepsen, L.O., Jensen, K.: Towards reachability trees for high–level petri nets. In: Rozenberg, G. (ed.) APN 1984. LNCS, vol. 188, pp. 215–233. Springer, Heidelberg (1985)
Ip, C.N., Dill, D.L.: Better verification through symmetry. Formal Methods in System Design 9, 41–75 (1996)
Kristensen, L.M., Mailund, T.: A generalized sweep-line method for safety properties. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 549–567. Springer, Heidelberg (2002)
Krisensen, L.M., Valmari, A.: Improved question-guided stubborn set methods for state properties. In: Proc. 21th Int. Conf. Application and Theory of Petri nets, pp. 282–302 (2000)
Mailund, T.: Sweeping the state space. PhD thesis, Univerity of Aarhus (2003)
Peled, D.: All from one, one for all: on model–checking using representitives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993)
Schmidt, K.: Lola: A low level analyser. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 465–474. Springer, Heidelberg (2000)
Schmidt, K.: Stubborn set for standard properties. In: Donatelli, S., Kleijn, J. (eds.) ICATPN 1999. LNCS, vol. 1639, pp. 46–65. Springer, Heidelberg (1999)
Schmidt, K.: How to calculate symmetries of petri nets. Acta Informatica 36, 545–590 (2000)
Schmidt, K.: Integrating low level symmetries into reachability analysis. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 315–331. Springer, Heidelberg (2000)
Tarjan, R.E.: Depth first search and linear graph algorithms. SIAM J. Comput. 1, 146–160 (1972)
Valmari, A.: Error detection by reduced reachability graph generation. In: Proc. of the 9th European Workshop on Application and Theory of Petri Nets, Venice (1988)
Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) APN 1990. LNCS, vol. 483, pp. 491–511. Springer, Heidelberg (1991)
Valmari, A.: On-the-fly verification with stubborn sets. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 397–408. Springer, Heidelberg (1993)
Valmari, A.: Stubborn set methods for process algebras. In: Workshop on Partial Order Methods in Verification, Princeton, pp. 192–210 (1996)
Valmari, A.: The state explosion problem. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 429–528. Springer, Heidelberg (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schmidt, K. (2004). Automated Generation of a Progress Measure for the Sweep-Line Method. In: Jensen, K., Podelski, A. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2004. Lecture Notes in Computer Science, vol 2988. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24730-2_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-24730-2_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21299-7
Online ISBN: 978-3-540-24730-2
eBook Packages: Springer Book Archive