ESTL: A temporal logic for events and states?

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.