Reachability in Two-Clock Timed Automata is PSPACE-complete
Formal Languages and Automata Theory
2020-01-15 v2
Abstract
A recent result of Haase et al. has shown that reachability in two-clock timed automata is log-space equivalent to reachability in bounded one-counter automata. We show that reachability in bounded one-counter automata is PSPACE-complete.
Cite
@article{arxiv.1302.3109,
title = {Reachability in Two-Clock Timed Automata is PSPACE-complete},
author = {John Fearnley and Marcin Jurdziński},
journal= {arXiv preprint arXiv:1302.3109},
year = {2020}
}