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.
Keywords Temporal logic - events - states - Petri nets - system development - specification - verification
Supported by the DFG within the research group “Petri Net Technology”