On parametric timed automata and one-counter machines

Ouaknine, J; Bundala, D

Journal article

On parametric timed automata and one-counter machines

Abstract:: Two decades ago, Alur, Henzinger, and Vardi introduced the reachability problem for parametric timed automata in the seminal paper. 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; (iiii) 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 PSPACE NEXP -hard respectively.

Publication status:: Published

Peer review status:: Peer reviewed

Actions

Email

Email this record

Send the bibliographic details of this record to your email address.

Your Email
Please enter the email address that the record information will be sent to.

-
Your message (optional)
Please add any additional information to be included within the email.
Share
Cite

Cite this record

APA Style

Ouaknine, J., & Bundala, D. (2016). On parametric timed automata and one-counter machines. Information and Computation, 253(2), 272–303.

MLA Style

Ouaknine, J, and D Bundala. “On Parametric Timed Automata and One-Counter Machines.” Information and Computation, vol. 253, no. 2, 2016, pp. 272–303.

Chicago Style

Ouaknine, J, and D Bundala. 2016. “On Parametric Timed Automata and One-Counter Machines.” Information and Computation 253 (2): 272–303.
Print