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 382-402. Lecture Notes in Computer Science 2075, edited by G. Goos, J. Hartmanis and J. van Leuwen, Springer, June 2001.
Abstract: We introduce partial S-invariants of Petri nets, which can help to determine invariants and to prove safety if large nets are built from smaller ones using parallel composition with synchronous communication. Partial S-invariants can support compositional reduction and, in particular, the fixed-point approach, used for verifying infinite parameterized families of concurrent systems. With partial S-invariants and the fixed-point approach we prove the correctness of two solutions to the MUTEX-problem based on token rings; for this, we only have to prove liveness of a simplified version due to previous results.