eng
episciences.org
Fundamenta Informaticae
0169-2968
1875-8681
2022-10-27
Volume 187, Issues 2-4: Petri...
10.46298/fi-2022-8878
8878
journal article
Computing Parameterized Invariants of Parameterized Petri Nets
Javier Esparza
Mikhail Raskin
Christoph Welzel
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.
https://fi.episciences.org/8878/pdf
Computer Science - Distributed, Parallel, and Cluster Computing
Computer Science - Multiagent Systems