In: H. Garavel, J. Hatcliff (Eds.): Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2003), 9th International Conference, Part of ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Volume 2619 of Lecture Notes in Computer Science, pages 442-457. Springer Verlag, February 2003.
Abstract: This paper is concerned with construction of some state space abstractions for Time Petri nets. State class spaces were introduced long ago by Berthomieu and Menasche as finite representations for the typically infinite state spaces of Time Petri nets, preserving their linear time temporal properties. This paper proposes a similar construction that preserves their branching time temporal properties. The construction improves a previous proposal by Yoneda and Ryuba. The method has been implemented, computing experiments are reported.
Keywords: Time Petri nets; state classes; branching time temporal properties; model-checking; bisimulation; real-time systems modeling and verification.