Reachability in two-clock timed automata is PSPACE-complete
From MaRDI portal
Publication:5327435
DOI10.1007/978-3-642-39212-2_21zbMATH Open1327.68118arXiv1302.3109OpenAlexW2046095317MaRDI QIDQ5327435FDOQ5327435
Authors: John Fearnley, Marcin Jurdziński 
Publication date: 7 August 2013
Published in: Automata, Languages, and Programming (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1302.3109
Recommendations
Formal languages and automata (68Q45) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)
Cited In (18)
- Timed network games with clocks
- Timed network games
- On the relationship between reachability problems in timed and counter automata
- Average-energy games
- Relating reachability problems in timed and counter automata
- Why liveness for timed automata is hard, and what we can do about it
- Quantum alternation
- Reachability in two-clock timed automata is PSPACE-complete
- Reachability in two-parametric timed automata with one parameter is EXPSPACE-complete
- Average-energy games
- On the decidability and complexity of problems for restricted hierarchical hybrid systems
- The complexity of flat freeze LTL
- Reachability games with relaxed energy constraints
- Parametrized automata simulation and application to service composition
- Reachability games with relaxed energy constraints
- Coverability in 2-VASS with one unary counter is in NP
- Title not available (Why is that?)
- On parametric timed automata and one-counter machines
This page was built for publication: Reachability in two-clock timed automata is PSPACE-complete
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5327435)
