Aufsatz![](/themes/Mirage2/images/Open_Access_logo_PLoS_transparent.svg)
Reachability in Two-Parametric Timed Automata with one Parameter is EXPSPACE-Complete
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 non-negative 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 PSPACENEXP. Our main result is that the reachability problem for two-parametric timed automata with one parameter is EXPSPACE-complete. Our contribution is two-fold. For the EXPSPACE lower bound, inspired by [13, 14], 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 one-counter automata over one parameter based on a minor adjustment of a construction due to Bundala and Ouaknine. For solving the reachability problem for parametric one-counter 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 doubly-exponential 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 long-standing open problem of reachability in parametric timed automata with two parametric clocks (and arbitrarily many parameters) and, if decidability holds, determinining its precise computational complexity.
Citation
In: Theory of Computing Systems Volume 68 / Issue 4 (2023-04-24) , S. 900 - 985 ; eissn:1433-0490Sponsorship
Gefördert im Rahmen des Projekts DEALCitation
@article{doi:10.17170/kobra-2024090610798,
author={Göller, Stefan and Hilaire, Mathieu},
title={Reachability in Two-Parametric Timed Automata with one Parameter is EXPSPACE-Complete},
journal={Theory of Computing Systems},
year={2023}
}
0500 Oax 0501 Text $btxt$2rdacontent 0502 Computermedien $bc$2rdacarrier 1100 2023$n2023 1500 1/eng 2050 ##0##http://hdl.handle.net/123456789/16028 3000 Göller, Stefan 3010 Hilaire, Mathieu 4000 Reachability in Two-Parametric Timed Automata with one Parameter is EXPSPACE-Complete / Göller, Stefan 4030 4060 Online-Ressource 4085 ##0##=u http://nbn-resolving.de/http://hdl.handle.net/123456789/16028=x R 4204 \$dAufsatz 4170 5550 {{Informatik}} 5550 {{Zeitsteuerung}} 5550 {{Automat}} 7136 ##0##http://hdl.handle.net/123456789/16028
2024-09-06T11:44:55Z 2024-09-06T11:44:55Z 2023-04-24 doi:10.17170/kobra-2024090610798 http://hdl.handle.net/123456789/16028 Gefördert im Rahmen des Projekts DEAL eng Namensnennung 4.0 International http://creativecommons.org/licenses/by/4.0/ Parametric timed automata Computational complexity Reachability EXPSPACE-complete 004 620 Reachability in Two-Parametric Timed Automata with one Parameter is EXPSPACE-Complete Aufsatz 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 non-negative 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 PSPACENEXP. Our main result is that the reachability problem for two-parametric timed automata with one parameter is EXPSPACE-complete. Our contribution is two-fold. For the EXPSPACE lower bound, inspired by [13, 14], 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 one-counter automata over one parameter based on a minor adjustment of a construction due to Bundala and Ouaknine. For solving the reachability problem for parametric one-counter 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 doubly-exponential 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 long-standing open problem of reachability in parametric timed automata with two parametric clocks (and arbitrarily many parameters) and, if decidability holds, determinining its precise computational complexity. open access Göller, Stefan Hilaire, Mathieu doi:10.1007/s00224-023-10121-3 Informatik Zeitsteuerung Automat publishedVersion eissn:1433-0490 Issue 4 Theory of Computing Systems 900 - 985 Volume 68 false
The following license files are associated with this item: