Partial S-invariants for the verification of infinite systems families

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. We show how partial S-invariants can support compositional reduction and, in particular, a specific form of it called the fixed-point approach. With the latter, infinite parameterized families of concurrent systems can be verified. Partial S-invariants and the fixed-point approach are used to 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