POST AND PRE-INITIALIZED STOPWATCH PETRI NETS

A modeling paradigm called Post and Pre-initialized Stopwatch Petri Nets (SWPN) is introduced. It extends Time Petri Nets TPN to the concept of stopwatch with an original mechanism of stopwatches reset. SWPN makes this reset dependent on the firing of the corresponding transitions. The resulting model permits natural description of so-called preemption-resume behavior. We give the formal semantics of SWPN as a timed transition system. We propose also a method for its analysis consisting in the computation of its equivalent stopwatch automaton SWA. The advantage of Petri Nets for modeling the complex system in concise way is combined with the power analysis of SWA.