Time Petri nets are Petri nets extended with a notion of time, where the occurrence time of a transition is constrained by a static interval. The objective of this work is to give time Petri nets a partial order semantics based on the nonsequential processes semantics for untimed net systems. A time process of a time Petri net is defined as a traditionally constructed causal process that has a valid timing. This means that the events of the process are labeled with occurrence times which must satisfy specific validness criteria. These criteria are obtained by analyzing how the timing constraints interact with the causal ordering of the events in the net. An efficient algorithm for checking then validness of a given timing is sketched. Interleavings of the time processes are defined as linearizations of the causal partial order of events where also the temporal ordering of events is preserved. The relationship between the firing schedules of a time Petri net and the interleavings of the time processes of the net is shown to be bijective. Also, a sufficient condition is given for when the invalidity of timings for a process can be inferred from an initial subprocess. An alternative characterization for the validness of timings then results in an algorithm for constructing the set of all valid timings for a process. This set of all valid timings is presented as sets of alternative linear constraints from which the existence of a valid timing can be decided.
@InProceedings{AurLil97,
author = {Tuomas Aura and Johan Lilius},
title = {Time processes of time Petri nets},
booktitle = {Proc.\ 18th Int.\ Conf.\ on Application and
Theory of Petri nets},
volume = 1248,
series = {LNCS},
pages = "136--155",
year = 1997,
publisher = {Springer Verlag},
month = jun
}