TCTL model checking of time Petri nets.

*(English)*Zbl 1188.68182Summary: 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.) |