Computing parameterized invariants of parameterized Petri nets

DOI10.1007/978-3-030-76983-3_8MaRDI QIDQ2117165zbMATH OpenOpenAlexFDO

Authors Javier Esparza, Mikhail Raskin, Christoph Welzel

Publication date 21 March 2022

Full work available at URL https://arxiv.org/abs/2103.10280

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

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.

Recommendations

Cites work

Cited in

(13)

Describes a project that uses

Uses Software

This page was built for publication: Computing parameterized invariants of parameterized Petri nets

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2117165)