Shrinking of Time Petri nets

The problem of the synthesis of time bounds enforcing good properties for reactive systems has been much studied in the literature. These works mainly rely on dioid algebra theory and require important restrictions on the structure of the model (notably by restricting to timed event graphs). In this paper, we address the problems of existence and synthesis of shrinkings of the bounds of the time intervals of a time Petri net, such that a given property is verified. We show that this problem is decidable for CTL properties on bounded time Petri nets. We then propose a symbolic algorithm based on the state class graph for a fragment of CTL. If the desired property “includes” k-boundedness, the proposed algorithm terminates even if the net is unbounded. A prototype has been implemented in our tool Romeo and the method is illustrated on a small case study from the literature.