For the most recent entries see the Petri Nets Newsletter.

ESTL: Some Proof Techniques.

Kindler, E.; Vesper, T.

In: W. van der Aalst, J.-M. Colom, F. Kordon, G. Kotsis and D. Moldt (Eds.): Petri Net Approaches for Modelling and Validation, Lincom Studies in Computer Science 01, pages 53-66. Lincom Europa, Munich, 2003, 2003.

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 on states as well as on events, which is called ESTL. This way, specifications in the early phases can be event-based and verification in later phases can be state-based within a single formalism. The emphasis of this paper, however, is on verification techniques for properties of a specific form. We present a simple technique based on the struture of the Petri net which, unfortunately, is not complete. Therefore, we present a second technique which reduces the verification of an event-based property to the verification of a state based property.

Keywords: Temporal logic, events, states, Petri nets, system development, specification, verification.


Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography