Javier Esparza ; Mikhail Raskin ; Christoph Welzel - Computing Parameterized Invariants of Parameterized Petri Nets

fi:8878 - Fundamenta Informaticae, October 27, 2022, Volume 187, Issues 2-4: Petri Nets 2021
Computing Parameterized Invariants of Parameterized Petri NetsArticle

Authors: 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.


    Volume: Volume 187, Issues 2-4: Petri Nets 2021
    Published on: October 27, 2022
    Accepted on: July 4, 2022
    Submitted on: December 21, 2021
    Keywords: Computer Science - Distributed, Parallel, and Cluster Computing,Computer Science - Multiagent Systems

    Consultation statistics

    This page has been seen 224 times.
    This article's PDF has been downloaded 168 times.