In: Desel, J.; Silva, M.: Lecture Notes in Computer Science, Vol. 1420: 19th Int. Conf. on Application and Theory of Petri Nets, ICATPN'98, Lisbon, Portugal, June 1998, pages 365-384. Berlin: Springer-Verlag, June 1998.
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, so 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.
Keywords: temporal logic; events; states; petri nets; system development; specification; verification.