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., 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 symbolic sets of valuations 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 sets of valuations arbitrarily close to the complete result. We demonstrate their applicability and efficiency using the tools Rom\'eo and IMITATOR on several benchmarks.

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