Ensuring the correctness of critical real-time systems, involving concurrent behaviors and timing requirements, is crucial. Timed automata extend finite-state automata with clocks, compared in guards and invariants with integer constants. Parametric timed automata (PTAs) extend timed automata with timing parameters. Parameter synthesis aims at computing dense sets of valuations for the timing parameters, guaranteeing a good behavior. However, in most cases, the emptiness problem for reachability (i.e., whether the emptiness of the parameter valuations set for which some location is reachable) is undecidable for PTAs and, as a consequence, synthesis procedures do not terminate in general, even for bounded parameters. In this paper, we introduce a parametric extrapolation, that allows us to derive an underapproximation in the form of linear constraints containing not only all the integer points ensuring reachability, but also all the (non-necessarily integer) convex combinations of these integer points, for general PTAs with a bounded parameter domain. We also propose two further algorithms synthesizing parameter valuations guaranteeing unavoidability, and preservation of the untimed behavior w.r.t. a reference parameter valuation, respectively. Our algorithms terminate and can output constraints arbitrarily close to the complete result. We demonstrate their applicability and efficiency using the tool Rom\'eo on two classical benchmarks.

翻译：确保涉及并发行为和时间约束的关键实时系统的正确性至关重要。时间自动机通过时钟扩展了有限状态自动机，并在守卫条件和不变式中与整数常量进行比较。参数时间自动机进一步扩展了时间自动机，引入了时间参数。参数综合旨在计算保证良好行为的时间参数估值稠密集。然而，在大多数情况下，对于参数时间自动机而言，可达性的空性问题（即是否存在参数估值集使得某个位置可达为空）不可判定，因此即使对于有界参数，综合过程通常也无法终止。本文提出了一种参数外推方法，对于具有有界参数域的一般参数时间自动机，该方法能够推导出一种线性约束形式的欠逼近，不仅包含所有确保可达性的整数点，还包括这些整数点的所有（不必然为整数的）凸组合。我们还提出了另外两种算法，分别用于综合保证不可避免性的参数估值，以及确保相对于参考参数估值的未定时行为保持不变。我们的算法可终止，并能输出任意接近完全结果的约束。通过工具Roméo在两个经典基准测试上的实验，我们展示了算法的适用性和效率。