In: J.-M. Colom, M. Koutny (Eds.), Newcastle upon Tyne, UK: Proc. of 22nd International Conf. on Applications and Theory of Petri Nets 2001 (ICATPN 2001), pages 323-342. Lecture Notes in Computer Science 2075, edited by G. Goos, J. Hartmanis and J. van Leuwen, Springer, June 2001.
Abstract: The paper deals with verification of untimed branching time properties of Time Petri Nets. The atomic variant of the geometric region method for preserving properties of CTL* and ACTL* is improved. Then, it is shown, for the first time, how to apply the partial order reduction method to deal with next-time free branching properties of Time Petri Nets. The above two results are combined offering an efficient method for model checking of ACTL*x and CTL*x properties of Time Petri Nets.