  Parametric timed automata are a powerful formalism for reasoning on
concurrent real-time systems with unknown or uncertain timing constants.
Reducing their state space is a significant way to reduce the inherently large
analysis times. We present here different merging reduction techniques based on
convex union of constraints (parametric zones), allowing to decrease the number
of states while preserving the correctness of verification and synthesis
results. We perform extensive experiments, and identify the best heuristics in
practice, bringing a significant decrease in the computation time on a
benchmarks library.
