Advances in Parametric Real-Time Reasoning

Abstract. We study the decidability and complexity of the reachability problem in parametric timed automata. The problem was introduced 20 years ago by Alur, Henzinger, and Vardi in [1], where they showed decidability in the case of a single parametric clock, and undecidability for timed automata with three or more parametric clocks. By translating such problems as reachability questions in certain ex-tensions of parametric one-counter machines, we show that, in the case of two parametric clocks (and arbitrarily many nonparametric clocks), reachability is decidable for parametric timed automata with a single parameter, and is moreover PSPACENEXP-hard. In addition, in the case of a single parametric clock (with arbitrarily many nonparametric clocks and arbitrarily many parameters), we show that the reachability problem is NEXP-complete, improving the nonelementary decision procedure of Alur et al.