On temporal logic programming using Petri nets

A methodology for modeling temporal (time-sensitive) aspects of discrete-event systems is presented. A formalism of temporal logic which incorporates both point and interval descriptions of time is formulated, which is an extension of Alien's interval logic. A formal axiomatic system of this point-interval logic is presented. A graph model is shown to implement the axiomatic system of point-interval logic. This graph-based approach transforms the system's specifications given by temporal statements into a graph structure. The graph-based temporal inference engine identifies temporal ambiguities and errors (if present) in the system's specifications, infers new temporal relations among system's intervals, and identifies the user-defined intervals of interest.