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.

翻译：对同时实时系统进行推理,其时间常数未知或不确定。 缩小其状态空间是减少固有大分析时间的重要途径。 我们在此提出不同的基于约束(对数区)曲线结合的合并削减技术,从而可以减少国家数量,同时保持核查和合成结果的正确性。 我们进行了广泛的实验,并找出了实践中的最佳超常性,大大缩短了基准图书馆的计算时间。