Parametric time Petri nets with inhibitor arcs (PITPNs) support flexibility for timed systems by allowing parameters in firing bounds. In this paper we present and prove correct a concrete and a symbolic rewriting logic semantics for PITPNs. We show how this allows us to use Maude combined with SMT solving to provide sound and complete formal analyses for PITPNs. We develop a new general folding approach for symbolic reachability that terminates whenever the parametric state-class graph of the PITPN is finite. We explain how almost all formal analysis and parameter synthesis supported by the state-of-the-art PITPN tool Rom\'eo can be done in 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 on three benchmarks show that our methods outperform Rom\'eo in many cases.

翻译：含抑制弧的参数化时间Petri网（PITPN）通过在触发边界中引入参数，为时间系统提供了灵活性。本文提出并证明了PITPN的具体与符号重写逻辑语义的正确性。我们展示了如何利用Maude结合SMT求解，为PITPN提供可靠且完备的形式化分析。针对符号可达性分析，我们提出了一种新的通用折叠方法，该方法可在PITPN的参数化状态类图有限时终止。我们阐明了如何通过Maude与SMT实现当前先进PITPN工具Roméo支持的几乎所有形式化分析与参数综合。此外，我们还支持从参数化初始标识出发的分析与参数综合，以及完整的LTL模型检验和基于用户定义执行策略的分析。在三个基准测试上的实验表明，我们的方法在多数情况下优于Roméo。