  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.
