Synthesizing Timed Transitions and Timed Places in a Petri Net

Abstract

Our research is to extend Petri nets by associating timing constraints with places and transitions in the original Petri nets, we called the extended places and transitions as timed places and timed transitions. respectively, and called the extended Petri nets as timing constraint Petri nets (TCPNs). TCPNs can be used to model and verify whether a real-time system specification satisfies the imposed timing constraints. Based on the definition of TCPNs, we have defined three synthesis rules-"sequential" synthesis rule, "or" synthesis rule, "and" synthesis rule to synthesize a time range. The time range can be either a span of fireable time (earliest and latest fireable times) associated with each timed transition or a span of enabling time (earliest and latest enabling times) associated with each timed places. A TCPN is verified to be satisfied with timing constraints if none of the synthesized spans of time is negative. The synthesis rules presented in this paper can be used not only in TCPNs, but also in other time-related extensions of Petri nets.