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.