Advances in parametric real-time reasoning

Daniel Bundala and Joël Ouaknine

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.