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 STOC 93, 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 extensions 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.
Proceedings of MFCS 14, LNCS 8634, 2014. 25 pages.
PDF © 2014 Springer-Verlag.