基于 Maude 与 SMT 求解的含抑制弧时间 Petri 网的符号分析与参数综合
计算机科学中的逻辑
2023-03-17 v1
摘要
带抑制弧的参数化时间 Petri 网（PITPNs）通过在触发界限中允许参数，为定时系统提供了灵活性。在本文中，我们提出并证明了 PITPNs 的具体重写逻辑语义和符号重写逻辑语义的正确性。我们展示了这如何使我们能够使用 Maude 结合 SMT 求解为 PITPNs 提供可靠且完备的形式化分析。我们开发了一种新的用于符号可达性的一般折叠方法，当 PITPN 的参数化状态类图有限时该方法终止。我们解释了最先进的 PITPN 工具 Roméo 所支持的几乎所有形式化分析和参数综合如何能在 Maude 中借助 SMT 完成。此外，我们还支持从参数化初始标识进行分析和参数综合，以及完整的 LTL 模型检验和带用户自定义执行策略的分析。在三个基准上的实验表明，我们的方法在许多情况下优于 Roméo。
引用
@article{arxiv.2303.08929,
title = {Symbolic Analysis and Parameter Synthesis for Time Petri Nets Using Maude and SMT Solving},
author = {Jaime Arias and Kyungmin Bae and Carlos Olarte and Peter Csaba Ölveczky and Laure Petrucci and Fredrik Rømming},
journal= {arXiv preprint arXiv:2303.08929},
year = {2023}
}