Reachability in two-clock timed automata is PSPACE-complete

DOI10.1007/978-3-642-39212-2_21MaRDI QIDQ5327435zbMATH OpenOpenAlexFDO

Authors John Fearnley, Marcin Jurdziński

Publication date 7 August 2013

Published in Automata, Languages, and Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1302.3109

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

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.

Recommendations

• Reachability in two-clock timed automata is PSPACE-complete
• Relating reachability problems in timed and counter automata
• On the relationship between reachability problems in timed and counter automata
• CONCUR 2004 - Concurrency Theory
• On parametric timed automata and one-counter machines

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
• Parametrized automata simulation and application to service composition
• Reachability games with relaxed energy constraints
• Reachability games with relaxed energy constraints
• Coverability in 2-VASS with one unary counter is in NP
• scientific article; zbMATH DE number 7559494 (Why is no real title available?)
• 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)