×

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.

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