Symbolic Unfolding of Parametric Stopwatch Petri Nets

International audienceWe 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 defi ne 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 fi nite complete pre fix of the symbolic unfolding. The originality of our work relies on a precise handling of direct conflicts between events, and the analysis of their eff ects on the constraints between the fi ring dates of those events