计算参数化Petri网的参数化不变量
Computing Parameterized Invariants of Parameterized Petri Nets
AI总结：
针对参数化Petri网，提出CEGAR循环构造有限参数化P-组件、虹吸管或陷阱集合，以无限实例证明安全性，弥补现有技术缺乏人类可理解解释的不足。
摘要：
Petri网模型的一个基本优势在于能够从网的语法自动计算有用的系统不变量。经典技术包括位置不变量、P-组件、虹吸管或陷阱。最近，Bozga等人提出了一种新技术，用于对具有环状或阵列架构的系统进行安全属性的参数化验证。他们表明，陈述“对于参数化Petri网的每个实例，满足与该实例所有P-组件、虹吸管和陷阱相关的线性不变量的所有标记都是安全的”可以用WS1S编码，并使用MONA等工具进行检查。然而，虽然该技术证明了从P-组件、虹吸管或陷阱中提取的无限线性不变量集合足以证明安全性，但它并未返回人类可理解的解释。我们提出了一个CEGAR循环，构造一个有限的参数化P-组件、虹吸管或陷阱集合，其无限多个实例足以证明安全性。为此，我们为不同架构设计了参数化程序。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
