zbMATH — the first resource for mathematics

TCTL model checking of time Petri nets. (English) Zbl 1188.68182
Summary: We consider Time Petri Nets (TPN) for which a firing time interval is associated with each transition. State space abstractions for TPN preserving various classes of properties (LTL, CTL and CTL*) can be computed, in terms of so-called state classes. Some methods were proposed to check quantitative timed properties but are not suitable for effective verification of properties of real-life systems. In this article, we consider subscript TCTL for TPN (TPN-TCTL) for which temporal operators are extended with a time interval, specifying a time constraint on the firing sequences. We prove the decidability of TPN-TCTL on bounded TPN and give its theoretical complexity. We propose a zone-based state space abstraction that preserves marking reachability and traces of the TPN. As for Timed Automata (TA), the abstraction may use an over-approximation operator on zones to enforce the termination. A coarser (and efficient) abstraction is then provided and proved exact w.r.t. marking reachability and traces (LTL properties). Finally, we consider a subset of TPN-TCTL properties (TPN-TCTLS) for which it is possible to propose efficient on-the-fly model-checking algorithms. Our approach consists in computing and exploring the zone-based state space abstraction. With a practical point of view, the method is integrated in Romeo [G. Gardey, D. Lime, M. Magnin and O. Roux, Lect. Notes Comput. Sci. 3576, 418–423 (2005; Zbl 1081.68618)], a tool for TPN edition and analysis. In addition to the old features it is now possible to effectively verify a subset of TCTL directly on TPN.

68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: DOI