Acta Informatica, 2024 (SCI-Expanded)
Parametric timed automata (PTA) extend timed automata (TA) with parameters instead of fixed timing constraints, providing the flexibility to accommodate uncertainties during the design phase. Once a parametric model is obtained, the next step is finding the optimal parameters such that the resulting TA satisfies the specifications. This paper introduces a new algorithm for determining parameters from safety specifications for PTA with bounded integer parameters and no nested cycles. The algorithm searches for unsafe paths through a depth-first search and generates parameter constraints. In particular, the realizability of simple and cyclic paths are encoded via mixed integer linear programming and non-linear programming problems. Then, the parameter constraints rendering the path unrealizable are derived via quantifier elimination. The accumulated constraints through the depth-first search guarantee that a parameter valuation satisfying these constraints solves the synthesis problem. The results are illustrated over benchmarks.