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

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

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

(21)

• Timed network games
• Reachability in two-clock timed automata is PSPACE-complete
• Quantum alternation
• Average-energy games
• Reachability games with relaxed energy constraints
• Relating reachability problems in timed and counter automata
• On the decidability and complexity of problems for restricted hierarchical hybrid systems
• Parametrized automata simulation and application to service composition
• On the relationship between reachability problems in timed and counter automata
• Timed network games with clocks
• Average-energy games
• Reachability games with relaxed energy constraints
• scientific article; zbMATH DE number 7559494 (Why is no real title available?)
• The complexity of flat freeze LTL
• Why liveness for timed automata is hard, and what we can do about it
• On parametric timed automata and one-counter machines
• Coverability in 2-VASS with one unary counter is in NP
• Reachability in two-parametric timed automata with one parameter is EXPSPACE-complete
• Coverability in VASS revisited: improving Rackoff's bounds to obtain conditional optimality
• Monus semantics in vector addition systems with states
• Temporal explorability games

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)