Reachability Problems and Abstract State Spaces for Time Petri Nets with Stopwatches

Bernard Berthomieu (1) , Didier Lime (2) , Olivier Henri Roux (2) , François Vernadat (1)

1 LAAS - Laboratoire d'analyse et d'architecture des systèmes
2 IRCCyN - Institut de Recherche en Communications et en Cybernétique de Nantes

Several extensions of Time Petri nets (TPNs) have been proposed for modeling suspension and resumption of actions in timed systems. We first introduce a simple class of TPNs extended with stopwatches (SwTPNs), and present a semi-algorithm for building exact representations of the behavior of SwTPNs, based on the known state class method for Time Petri nets. Then, we prove that state reachability in SwTPNs and all similar models is undecidable, even when bounded, which solves an open problem. Finally, we discuss overapproximation methods yielding finite abstractions of their behavior for a subclass of bounded SwTPNs, and propose a new one based on a quantization of the polyhedra representing temporal information. By adjusting a parameter, the exact behavior can be approximated as closely as desired. The methods have been implemented, experiments are reported.

Mots clés: Time Petri nets; Stopwatches; State classes; Reachability; Decidability; Approximation; Real-time systems modeling and verification

Domaines: Autre [cs.OH]

Bernard Berthomieu, Didier Lime, Olivier Henri Roux, François Vernadat. Reachability Problems and Abstract State Spaces for Time Petri Nets with Stopwatches. Discrete Event Dynamic Systems, 2007, 17 (2), pp.133-158. ⟨10.1007/s10626-006-0011-y⟩. ⟨hal-00489016⟩