Reachability in Two-Clock Timed Automata is PSPACE-complete
John Fearnley, Marcin Jurdzi\'nski
TL;DR
This paper proves that the reachability problem in bounded one-counter automata, which is equivalent to two-clock timed automata, is PSPACE-complete, establishing its computational complexity.
Contribution
It demonstrates that reachability in bounded one-counter automata is PSPACE-complete, resolving an open complexity question for two-clock timed automata.
Findings
Reachability in bounded one-counter automata is PSPACE-complete.
Two-clock timed automata reachability is PSPACE-complete due to their equivalence.
The complexity class of the problem is established as PSPACE-complete.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.