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 242-262. Lecture Notes in Computer Science 2075, edited by G. Goos, J. Hartmanis and J. van Leuwen, Springer, June 2001.
Abstract: Latvala and Heljanko have presented how model checking of linear temporal logic properties of P/T nets with fairness constraints on the transitions can be done efficiently. In this work the procedure is extended to high-level Petri Nets, Coloured Petri Nets in particular. The model checking procedure has been implemented in the MARIA tool. As a case study, a liveness property of a sliding window protocol is model checked. The results indicate that the procedure can cope well with many fairness constraints, which could not have been handled by specifying the constraints as a part of the property to be verified.
Keywords: Model checking, fairness, LTL, high-level Petri Nets.