Abstract
One of the most efficient analysis technique is to reduce an original model into a simpler one such that the reduced model has the same properties than the original one. G. Berthelot defined in this thesis some reductions of Petri nets that are based on local structural conditions and that simplify significantly the net. However, the author focused only on the preservation of classical properties (such that liveness, boundedness, ...) that are not necessarily the most useful in practice. In this paper, we prove that two of these structural reductions (the pre and post transitions agglomerations) preserve also a large set of properties expressed in linear-time temporal logics under simple conditions.
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. Checking properties of nets using transformations. In G. Rozenberg, editor, Advances in Petri nets, volume No. 222 of LNCS. Springer-Verlag, 1985.
S. Haddad. A reduction theory for colored nets. In Jensen and Rozenberg, editors, High-level Petri Nets, Theory and Application, LNCS, pages 399–425. Springer-Verlag, 1991.
Doron Peled and Thomas Wilke. Stutter-invariant temporal properties are expressible without the nexttime operator. Information Processing Letters, 63:243–246, 1997.
W. Reisig. EATCS-An Introduction to Petri Nets. Springer-Verlag, 1983.
A. Valmari. On-the-fly verification with stubborn sets representatives. In Proceedings of the 5th International Conference on Computer Aided Verification, Greece, volume 697 of Lecture Notes in Computer Science, pages 397–408. Springer Verlag, 1993.
K. Varpaaniemi and M. Rauhamaa. The stubborn set method in practice. In Advances in Petri Nets, volume 616 of Lecture Notes in Computer Science, pages 389–393. Springer Verlag, 1992.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Poitrenaud, D., Pradat-Peyre, JF. (2000). Pre- and Post-agglomerations for LTL Model Checking. In: Nielsen, M., Simpson, D. (eds) Application and Theory of Petri Nets 2000. ICATPN 2000. Lecture Notes in Computer Science, vol 1825. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44988-4_22
Download citation
DOI: https://doi.org/10.1007/3-540-44988-4_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67693-5
Online ISBN: 978-3-540-44988-1
eBook Packages: Springer Book Archive