Two decades ago, Alur, Henzinger, and Vardi introduced the
reachability problem for parametric timed automata in the seminal
paper [2]. Their main results are that reachability is decidable for
timed automata with a single parametric clock, and undecidable for
timed automata with three or more parametric clocks.
In the case of two parametric clocks, decidability was left open, with
hardly any progress (partial or otherwise) that we are aware of in the
intervening period. As pointed out by Alur et al., this case
also subsumes Ibarra et al.'s reachability problem for "simple
programs" [14], another long-standing open problem, as well as the
decision problem for a fragment of Presburger arithmetic with
divisibility.
In this manuscript we establish a correspondence between reachability
in parametric timed automata with at most two parametric clocks (and
arbitrarily many nonparametric clocks) and reachability for a certain
class of parametric one-counter machines. We then leverage this
connection (i) to improve Alur et al.'s decision procedure
for one parametric clock from nonelementary to 2NEXP; (ii) to
show decidability for two parametric clocks provided the timed
automaton uses only a single parameter; (iii) to show decidability
for various resulting classes of parametric one-counter machines; and
(iv) to show decidability of reachability for the simple programs of
Ibarra et al. in the presence of a single parameter. In addition, we
prove that for one and two parametric clocks the reachability problem
is NEXP-hard and PSPACENEXP-hard respectively.
Information and Computation 253, 2017. 40 pages.
PDF
© 2016 Elsevier Inc.