{"docId":10196,"paperId":8878,"url":"https:\/\/fi.episciences.org\/8878","doi":"","journalName":"Fundamenta Informaticae","issn":"0169-2968","eissn":"1875-8681","volume":[{"vid":590,"name":"Volume 187, Issues 2-4: Petri Nets 2021"}],"section":[],"repositoryName":"arXiv","repositoryIdentifier":"2103.10280","repositoryVersion":7,"repositoryLink":"https:\/\/arxiv.org\/abs\/2103.10280v7","dateSubmitted":"2021-12-21 08:05:37","dateAccepted":"2022-07-04 19:34:45","datePublished":"2022-10-27 09:05:38","titles":["Computing Parameterized Invariants of Parameterized Petri Nets"],"authors":["Esparza, Javier","Raskin, Mikhail","Welzel, Christoph"],"abstracts":["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.","Comment: Final version from editor"],"keywords":["Computer Science - Distributed, Parallel, and Cluster Computing","Computer Science - Multiagent Systems"]}