Volume 17, Number 2, 133-158, DOI: 10.1007/s10626-006-0011-y

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

Bernard Berthomieu, Didier Lime, Olivier H. Roux and François Vernadat

From the issue entitled "Modelling and Control of Reactive Systems, Guest Editors: Hassane Alla, René Boel, Eric Rutten"

View Related Documents

Abstract

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.

Keywords  Time Petri nets - Stopwatches - State classes - Reachability - Decidability - Approximation - Real-time systems modeling and verification

Fulltext Preview

Image of the first page of the fulltext document