Abstract
In some phases of system development state-based methods are adequate; in others event-based methods are adequate. Petri nets provide a system model which supports both methods and thus allow a smooth transition between the different phases of system development. Most temporal logics for Petri nets, however, do not support both methods.
In this paper we introduce a temporal logic for Petri nets which allows to argue about states as well as to argue about events. This way, specifications in the early phases can be event-based and verification in later phases can be state-based within a single formalism.
Supported by the DFG within the research group “Petri Net Technology”
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Wil van der Aalst. Three good reasons for using a Petri-net-based workflow management system. In S. Navathe and T. Wakayama, editors, Proceedings of the International Working Conference on Information and Process Integration in Enterprises, pages 179–201, Cambridge, Massachusetts, 1996.
Eike Best and César Fernández. Nonsequential Processes, EATCS Monographs on Theoretical Computer Science 13. Springer-Verlag, 1988.
Felix Cornelius, Heinrich Hußmann, and Michael Löwe. The KORSO case study for software engineering with formal methods: A medical information system. In M. Broy and S. Jähnichen, editors, KORSO: Methods, Languages, and Tools for the Construction of Correct Software, LNCS 1009, pages 417–445. Springer-Verlag, 1995.
Claudia Ermel, Magdalena Gajewsky, Tobias Vesper, and Michael Weber. Verifikation strukturierter Netze. In H. Weber, H. Ehrig, and W. Reisig, editors, Move-On-Workshop, DFG-Forschergruppe Petri Net Technology. Technical University Berlin, 1997.
Ursula Goltz and Wolfgang Reisig. The non-sequential behaviour of Petri nets. Information and Control, 57:125–147, 1983.
Ekkart Kindler and Wolfgang Reisig. Algebraic system nets for modelling distributed algorithms. Petri Net Newsletter, 51:16–31, 1996.
Ekkart Kindler, Wolfgang Reisig, Hagen Völzer, and Rolf Walter. Petri net based verification of distributed algorithms: An example. Formal Aspects of Computing, 9:409–424, 1997.
Ekkart Kindler and Tobias Vesper. A temporal logic for events and states in Petri nets. In B. Farwer, D. Moldt, and M.-O. Stehr, editors, Petri Nets in System Engineering, pages 101–110, Hamburg, 1997.
David A. Marca and Clement L. McGowan. SADT: Structured Analysis and Design Technique. McGraw-Hill, 1988.
Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Specification. Springer-Verlag, 1992.
Wolfgang Reisig. Petri Nets, EATCS Monographs on Theoretical Computer Science 4. Springer-Verlag, 1985.
Wolfgang Reisig. Petri nets and algebraic specifications. Theoretical Computer Science, 80:1–34, 1991.
Wolfgang Reisig. Petri net models of distributed algorithms. In J. van Leeuven, editor, Computer Science Today: Recent Trends and Developments, LNCS 1000, pages 441–454. Springer-Verlag, Berlin, 1995.
Wolfgang Reisig. Interleaved progress, concurrent progress, and local progress. In D.A. Peled, V.R. Pratt, and G.J. Holzmann, editors, Partial Order Methods in Verification, DIMACS Series in Discrete Mathematics and Theoretical Computer Science 29, pages 99–115. AMS, 1997.
Wolfgang Reisig. Elements of Distributed Algorithms. Modeling and Analysis with Petri Nets. In preparation, Springer-Verlag, 1998.
Douglas T. Ross. Structured Analysis (SA): A language for communicating ideas. IEEE Software Engineering Transactions, 3(1):16–37, January 1977.
Antonia Sinachopoulos. Temporal logics of elementary net systems. Arbeitspapiere der GMD 353, 1988.
Michael Weber, Rolf Walter, Hagen Völzer, Tobias Vesper, Wolfgang Reisig, Sibylle Peuker, Ekkart Kindler, Jörn Freiheit, and Jörg Desel. DAWN: Petrinetzmodelle zur Verifikation Verteilter Algorithmen. Informatik-Bericht 88, Humboldt-University Berlin, December 1997.
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
Kindler, E., Vesper, T. (1998). ESTL: A Temporal Logic for Events and States. 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_20
Download citation
DOI: https://doi.org/10.1007/3-540-69108-1_20
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