Computing Parameterized Invariants of Parameterized Petri Nets

TL;DR

This paper introduces a CEGAR-based method to compute finite, parameterized invariants for Petri nets, enabling human-understandable proofs of safety across all instances of parameterized systems.

Contribution

It presents a novel CEGAR loop that constructs finite sets of parameterized invariants, enhancing the verification of safety properties in parameterized Petri nets.

Findings

Successfully constructs finite parameterized invariants.

Proves safety for all instances of parameterized Petri nets.

Designs parameterization procedures for various architectures.

Abstract

A fundamental advantage of Petri net models is the possibility to automatically compute useful system invariants from the syntax of the net. Classical techniques used for this are place invariants, P-components, siphons or traps. Recently, Bozga et al. have presented a novel technique for the \emph{parameterized} verification of safety properties of systems with a ring or array architecture. They show that the statement \enquote{for every instance of the parameterized Petri net, all markings satisfying the linear invariants associated to all the P-components, siphons and traps of the instance are safe} can be encoded in \acs{WS1S} and checked using tools like MONA. However, while the technique certifies that this infinite set of linear invariants extracted from P-components, siphons or traps are strong enough to prove safety, it does not return an explanation of this fact understandable by humans. We present a CEGAR loop that constructs a \emph{finite} set of \emph{parameterized} P-components, siphons or traps, whose infinitely many instances are strong enough to prove safety. For this we design parameterization procedures for different architectures.