Date: August 1996
Pages: 58
The objective of this thesis is to give time Petri nets a partial order semantics, like the nonsequential processes of untimed net systems. A time process of a time Petri net is defined as a traditionally constructed causal process with a valid timing. This means that the events of the process are labeled with occurrence times which must satisfy specific validness criteria. An efficient algorithm for checking validness of known timings is presented. Interleavings of the time processes are defined as linearizations of the causal partial order of events where also the time order of events is preserved. The relationship between 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 its initial subprocess. An alternative characterization for the validness of timings results in an algorithm for constructing the set of all valid timings for a process. The set of all valid timings is presented as sets of alternative linear constraints, which can be used in optimization problems. The techniques developed can be used to compute, for example, the maximum time separation of two events in a process. The existence of a valid timing for a given process can be decided in NP time.
Keywords: Time Petri nets, processes, timing analysis, partial order semantics, causality, net theory.