Abstract
The sweep-line method is a state space exploration method for on-the-fly verification aimed at systems exhibiting progress. Presence of progress in the system makes it possible to delete certain states during state space generation, which reduces the memory used for storing the states. Unfortunately, the same progress that is used to improve memory performance in state space exploration often leads to an infinite state space: The progress in the system is carried over to the states resulting in infinitely many states only distinguished through the progress. A finite state space can be obtained using equivalence reduction, abstracting away the progress, but in its simplest form this removes the progress property required by the sweep-line method. In this paper we examine a new method for using equivalence relations to obtain a finite set of classes, without compromising the progress property essential for the sweep-line method. We evaluate the new method on two case studies, showing significant improvements in performance, and we briefly discuss the new method in the context of Timed Coloured Petri Nets, where the “increasing global time” semantics can be exploited for more efficient analysis than what is achieved using a “delay” semantics.
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
G. Berthelot. Occurrence Graphs for Interval Timed Coloured Nets. In Proceedings of ICATPN’94, volume 815 of Lecture Notes in Computer Science, pages 79–98. Springer Verlag, 1994.
D. Bertsekas and R. Gallager. Data Networks. Prentice-Hall, Inc., 1992.
S. Christensen, K. Jensen, and L.M. Kristensen. Design/CPN Occurrence Graph Manual. Department of Computer Science, University of Aarhus, Denmark. Online version: http://www.daimi.au.dk/designCPN/.
S. Christensen, K. Jensen, T. Mailund, and L. M. Kristensen. State Space Methods for Timed Coloured Petri Nets. In Proceedings of 2nd International Colloquium on Petri Net Technologies for Modelling Communication Based Systems, Berlin Germany, September 2001.
S. Christensen and J. B. Jørgensen. Analysis of Bang and Olufsen’s BeoLink Audio/Video System Using Coloured Petri Nets. In P. Azéma and G. Balbo, editors, Proceedings of ICATPN’97, volume 1248 of Lecture Notes in Computer Science, pages 387–406. Springer-Verlag, 1997.
S. Christensen, J. B. Jørgensen, and L. M. Kristensen. Design/CPN-A Computer Tool for Coloured Petri Nets. In E. Brinksma, editor, Proceedings of TACAS’97, volume 1217 of Lecture Notes in Computer Science, pages 209–223. Springer-Verlag, 1997.
S. Christensen, L. M. Kristensen, and T. Mailund. A Sweep-Line Method for State Space Exploration. In Tiziana Margaria and Wang Yi, editors, Proceedings of TACAS’01, volume 2031 of Lecture Notes in Computer Science, pages 450–464. Springer-Verlag, 2001.
S. Christensen, L.M. Kristensen, and T. Mailund. Condensed State Spaces for Timed Petri Nets. In José-Manuel Colom and Maciej Koutny, editors, Proceedings of ICATPN’01, volume 2075 of Lecture Notes in Computer Science, pages 101–120. Springer-Verlag, 2001.
E. M. Clarke, R. Enders, T. Filkorn, and S. Jha. Exploiting Symmetries in Temporal Logic Model Checking. Formal Methods in System Design, 9, 1996.
E. A. Emerson and A. P. Sistla. Symmetry and Model Checking. Formal Methods in System Design, 9, 1996.
K. Jensen. Coloured Petri Nets-Basic Concepts, Analysis Methods and Practical Use.-Volume 1: Basic Concepts. Monographs in theoretical computer science, Springer-Verlag, Berlin, 1992.
K. Jensen. Coloured Petri Nets-Basic Concepts, Analysis Methods and Practical Use.-Volume 2: Analysis Methods. Monographs in theoretical computer science, Springer-Verlag, Berlin, 1994.
K. Jensen. Condensed State Spaces for Symmetrical Coloured Petri Nets. Formal Methods in System Design, 9, 1996.
J. B. Jørgensen and L. M. Kristensen. Design/CPN Condensed State Space Tool Manual Department of Computer Science, University of Aarhus, Denmark, 1996. Online: http://www.daimi.au.dk/designCPN/.
L. M. Kristensen, S. Christensen, and K. Jensen. The Practitioner’s Guide to Coloured Petri Nets. International Journal on Software Tools for Technology Transfer, 2(2):98–132, December 1998.
Design/CPN Online. http://www.daimi.au.dk/designCPN/.
W. M. P. van der Aalst. Interval Timed Coloured Petri Nets and their Analysis. In Proceedings of ICATPN’93, volume 691 of Lecture Notes in Computer Science, pages 453–472. Springer Verlag, 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mailund, T. (2002). Analysing Infinite-State Systems by Combining Equivalence Reduction and the Sweep-Line Method. In: Esparza, J., Lakos, C. (eds) Application and Theory of Petri Nets 2002. ICATPN 2002. Lecture Notes in Computer Science, vol 2360. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48068-4_19
Download citation
DOI: https://doi.org/10.1007/3-540-48068-4_19
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43787-1
Online ISBN: 978-3-540-48068-6
eBook Packages: Springer Book Archive