Abstract
Parametric timed automata (PTA) have been introduced by Alur, Henzinger, and Vardi as an extension of timed automata in which clocks can be compared against parameters. The reachability problem asks for the existence of an assignment of the parameters to the nonnegative integers such that reachability holds in the underlying timed automaton. The reachability problem for PTA is long known to be undecidable, already over three parametric clocks.
A few years ago, Bundala and Ouaknine proved that for PTA over two parametric clocks and one parameter the reachability problem is decidable and also showed a lower bound for the complexity class PSPACE^NEXP. Our main result is that the reachability problem for parametric timed automata over two parametric clocks and one parameter is EXPSPACEcomplete.
For the EXPSPACE lower bound we make use of deep results from complexity theory, namely a serializability characterization of EXPSPACE (in turn based on Barrington’s Theorem) and a logspace translation of numbers in Chinese Remainder Representation to binary representation due to Chiu, Davida, and Litow. It is shown that with small PTA over two parametric clocks and one parameter one can simulate serializability computations.
For the EXPSPACE upper bound, we first give a careful exponential time reduction from PTA over two parametric clocks and one parameter to a (slight subclass of) parametric onecounter automata over one parameter based on a minor adjustment of a construction due to Bundala and Ouaknine. For solving the reachability problem for parametric onecounter automata with one parameter, we provide a series of techniques to partition a fictitious run into several carefully chosen subruns that allow us to prove that it is sufficient to consider a parameter value of exponential magnitude only. This allows us to show a doublyexponential upper bound on the value of the only parameter of a PTA over two parametric clocks and one parameter. We hope that extensions of our techniques lead to finally establishing decidability of the longstanding open problem of reachability in parametric timed automata with two parametric clocks (and arbitrarily many parameters) and, if decidability holds, determining its precise computational complexity.
BibTeX  Entry
@InProceedings{goller_et_al:LIPIcs.STACS.2021.36,
author = {G\"{o}ller, Stefan and Hilaire, Mathieu},
title = {{Reachability in TwoParametric Timed Automata with One Parameter Is EXPSPACEComplete}},
booktitle = {38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021)},
pages = {36:136:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959771801},
ISSN = {18688969},
year = {2021},
volume = {187},
editor = {Bl\"{a}ser, Markus and Monmege, Benjamin},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/13681},
URN = {urn:nbn:de:0030drops136817},
doi = {10.4230/LIPIcs.STACS.2021.36},
annote = {Keywords: Parametric Timed Automata, Computational Complexity, Reachability}
}
Keywords: 

Parametric Timed Automata, Computational Complexity, Reachability 
Collection: 

38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021) 
Issue Date: 

2021 
Date of publication: 

10.03.2021 