  Timed automata (TAs) are an efficient formalism to model and verify systems
with hard timing constraints, and concurrency. While TAs assume exact timing
constants with infinite precision, parametric TAs (PTAs) leverage this
limitation and increase their expressiveness, at the cost of undecidability. A
practical explanation for the efficiency of TAs is zone extrapolation, where
clock valuations beyond a given constant are considered equivalent. This
concept cannot be easily extended to PTAs, due to the fact that parameters can
be unbounded. In this work, we propose several definitions of extrapolation for
PTAs based on the M-extrapolation, and we study their correctness. Our
experiments show an overall decrease of the computation time and, most
importantly, allow termination of some previously unsolvable benchmarks.
