A causal semantics for time Petri nets

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.