Symbolic unfolding of parametric stopwatch Petri nets

Research paper by Claude Jard, Didier Lime, Olivier H. Roux, Louis-Marie Traonouez

Indexed on: 15 May '13Published on: 15 May '13Published in: Formal Methods in System Design


We address the problem of unfolding safe parametric stopwatch time Petri nets (PSwPNs), i.e., safe time Petri nets (TPNs) possibly extended with time parameters and stopwatches. We extend the notion of branching process to account for the dates of the occurrences of events and thus define a symbolic unfolding for PSwPNs. In the case of TPNs we also propose a method based on our so-called time branching processes to compute a finite complete prefix of the symbolic unfolding. The originality of our work relies on a precise handling of direct conflicts between events, and the analysis of their effects on the constraints between the firing dates of those events.