Characterization of timed well-formed Petri nets behavior by means of occurrence equations

So called “recursive equations” have been introduced by Baccelli et al. (1992) as a convenient way of characterizing the behavior of stochastic Petri net models in terms of transition firing instances and of creation and destruction times for tokens in places. Such equations have been used to prove model properties as well as to speed up simulation by parallel processing techniques in the case of marked graph structures with FIFO token flow. We extend the technique to the case of high-level net models in which conflicts among transitions and firing disciplines different from FIFO are allowed. We propose the new name of “occurrence equations” to characterize the technique more precisely. Different execution policies that have been considered in the literature are discussed, showing the consequences they induce on the net occurrence equations