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.

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