This paper presents a concrete and a symbolic rewriting logic semantics for parametric time Petri nets with inhibitor arcs (PITPNs), a flexible model of timed systems where parameters are allowed in firing bounds. We prove that our semantics is bisimilar to the "standard" semantics of PITPNs. This allows us to use the rewriting logic tool Maude, combined with SMT solving, to provide sound and complete formal analyses for PITPNs. We develop and implement a new general folding approach for symbolic reachability, so that Maude-with-SMT reachability analysis terminates whenever the parametric state-class graph of the PITPN is finite. Our work opens up the possibility of using the many formal analysis capabilities of Maude -- including full LTL model checking, analysis with user-defined analysis strategies, and even statistical model checking -- for such nets. We illustrate this by explaining how almost all formal analysis and parameter synthesis methods supported by the state-of-the-art PITPN tool Romeo can be performed using Maude with SMT. In addition, we also support analysis and parameter synthesis from parametric initial markings, as well as full LTL model checking and analysis with user-defined execution strategies. Experiments show that our methods outperform Romeo in many cases.

翻译：本文提出了一种针对带抑制弧的参量时间佩特里网（PITPN）的具体化与符号化重写逻辑语义——PITPN是一种灵活的定时系统模型，其中触发界允许参量化。我们证明该语义与PITPN的“标准”语义是互模拟等价的。这使得我们能够结合重写逻辑工具Maude与SMT求解，为PITPN提供可靠且完备的形式化分析。我们为符号可达性开发并实现了一种新型通用折叠方法，使得当PITPN的参量状态类图有限时，基于Maude与SMT的可达性分析能够终止。我们的工作开创了将Maude的多种形式化分析能力（包括完整LTL模型检验、用户自定义策略分析乃至统计模型检验）应用于此类网的可能性。我们通过阐述如何利用Maude结合SMT实现当前最先进的PITPN工具Romeo所支持的几乎所有形式化分析与参数综合方法，对此进行了说明。此外，我们还支持从参量初始标识出发的分析与参数综合，以及完整LTL模型检验和用户自定义执行策略分析。实验表明，我们的方法在多数情况下优于Romeo。