Robustness of Time Petri Nets under Guard Enlargement

International audienceRobustness of timed systems aims at studying whether infinitesimal perturbations inclock values can result in new discrete behaviors. A model is robust if the set of discrete behav-iors is preserved under arbitrarily small (but positive) perturbations. We tackle this problem for timePetri nets (TPNs, for short) by considering the model of parametric guard enlargement which allowstime-intervals constraining the firing of transitions in TPNs to be enlarged by a (positive) parameter.We show that TPNs are not robust in general and checking if they are robust with respect to standardproperties (such as boundedness, safety) is undecidable. We then extend the marking class timedautomaton construction for TPNs to a parametric setting, and prove that it is compatible with guardenlargements. We apply this result to the (undecidable) class of TPNs which are robustly bounded(i.e., whose finite set of reachable markings remains finite under infinitesimal perturbations): weprovide two decidable robustly bounded subclasses, and show that one can effectively build a timedautomaton which is timed bisimilar even in presence of perturbations. This allows us to applyexisting results for timed automata to these TPNs and show further robustness properties