A causal semantics for time Petri nets

A1 Journal article (refereed)

Internal Authors/Editors

Publication Details

List of Authors: Tuomas Aura, Johan Lilius
Publication year: 2000
Journal: Theoretical Computer Science
Volume number: 243
Issue number: 1-2
Start page: 409
End page: 447
ISSN: 0304-3975


The objective of this work is to give time Petri nets a partial order semantics, akin to the nonsequential processes of untimed net systems. To this end a time process of a time Petri net is defined as a traditionally constructed causal process with a valid timing. A timing is a labelling that attaches occurrence times to the events of the process that must satisfy specific validness criteria. The main result of the paper is the bijective correspondence between firing schedules (the classical interleaving semantics of time Petri nets) and linearizations of time processes. The result shows that time processes correctly represent the behavior of the system. Using the definition of validness, an efficient algorithm for checking validness of given timings is derived. Also a sufficient condition is given for when the invalidity of timings for a process can be inferred from its initial subprocess. To compute, e.g. the maximum time separation between two events in a time process an alternative characterization of validness is developed. This definition is used to derive an algorithm for constructing the set of all valid timings for a process. The set of valid timings is presented as sets of alternative linear constraints, which can be used in optimization problems. It is shown that the existence of a valid timing for a given process can be decided in NP time.

Last updated on 2020-15-08 at 05:05