参数化 Petri 网的参数化不变量计算

Petri 网模型的一个基本优势是能够从网的语法自动计算有用的系统不变量。用于此的经典技术包括位置不变量、P-分量、虹吸或陷阱。近来，Bozga 等人提出了一种用于具有环形或阵列架构系统的参数化安全性验证的新技术。他们表明，命题“对于参数化 Petri 网的每个实例，所有满足该实例的所有 P-分量、虹吸与陷阱所关联线性不变量的标记都是安全的”可被编码于 \acs{WS1S} 中，并使用如 MONA 等工具进行查验。然而，尽管该技术证明了从 P-分量、虹吸或陷阱提取的此无限线性不变量集合足以证明安全性，它并未给出人类可理解的对此事实的解释。我们提出了一个 CEGAR 循环，其构造出一个有限的参数化 P-分量、虹吸或陷阱集合，其无限多个实例足以证明安全性。为此，我们为不同架构设计了参数化过程。