In: Proceedings of Applications and Theory of Petri Nets 2004: 25th International Conference, ICATPN 2004, Bologna, Italy, June 21-25, 2004, pages 37-76. Volume 3099 of Lecture Notes in Computer Science / Cortadella, Reisig (Eds.) --- Springer-Verlag, September 2004.
Abstract: The paper surveys some of the most recent approaches to verification of properties, expressible in some timed and untimed temporal logics (LTL, CTL, TCTL), for real-time systems represented by time Petri nets (TPN's) and timed automata (TA). Firstly, various structural translations from TPN's to TA are discussed. Secondly, model abstraction methods, based on state class approaches for TPNrsquos, and on partition refinement for TA, are given. Next, SAT-based verification techniques, like bounded and unbounded model checking, are discussed. The main focus is on bounded model checking for TCTL and for reachability properties. The paper ends with a comparison of experimental results for several time Petri nets, obtained using the above solutions, i.e., either model abstractions for TPN's, or a translation of a net to a timed automaton and then verification methods for TA. The experiments have been performed using some available tools for TA and TPN's.