Symbolic Model Checking for Timed Petri Nets

Symbolic model checking is a powerful technique for checking temporal logic properties over finite operational models. Recently, symbolic model checking has been extended to timed models to check temporal properties of real-time system. Real-time extensions of symbolic model checking require the description of the state space of the system to be analyzed in specific forms of timed graphs. This paper presents a symbolic model checking algorithm for analyzing specifications of real-time systems expressed in an intuitive and popular model, namely timed Petri nets. The algorithm proposed in this paper checks the validity of properties expressed in TCTL on the time reachability graph of timed Petri nets. A realistic example illustrates how the algorithm proposed in this paper can be successfully used in practical applications despite the worst case computational complexit