Reachability in two-clock timed automata is PSPACE-complete

DOI10.1016/J.IC.2014.12.004MaRDI QIDQ2347796zbMATH OpenOpenAlexFDO

Authors John Fearnley, Marcin Jurdziński

Publication date 9 June 2015

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ic.2014.12.004

zbMATH Keywords

counter automataPSPACE-completetimed automata

Mathematics Subject Classification ID

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

Recommendations

• Reachability in two-clock timed automata is PSPACE-complete
• Reachability relations of timed pushdown automata
• scientific article; zbMATH DE number 1796157
• scientific article; zbMATH DE number 7297846
• scientific article; zbMATH DE number 5024617
• Binary reachability of timed pushdown automata via quantifier elimination and cyclic order atoms
• scientific article; zbMATH DE number 1670769
• Timed Pushdown Automata Revisited
• Timed P Automata
• Timed P automata

Cites work

• A theory of timed automata
• CONCUR 2004 - Concurrency Theory
• Infinite Runs in Weighted Timed Automata with Energy Constraints
• Minimum and maximum delay problems in real-time systems
• On the relationship between reachability problems in timed and counter automata
• Reachability in Succinct and Parametric One-Counter Automata
• The complexity of membership problems for circuits over sets of integers

Cited in

(28)

• Reachability relations of timed pushdown automata
• Relating reachability problems in timed and counter automata
• Bounding Average-Energy Games
• Model checking flat Freeze LTL on one-counter automata
• On the relationship between reachability problems in timed and counter automata
• Regular separability of one counter automata
• On Affine Reachability Problems
• Universality Problem for Unambiguous VASS
• scientific article; zbMATH DE number 7559493 (Why is no real title available?)
• scientific article; zbMATH DE number 7559498 (Why is no real title available?)
• Determinisability of register and timed automata
• Life is random, time is not: Markov decision processes with window objectives
• Reachability in two-clock timed automata is PSPACE-complete
• Life is random, time is not: Markov decision processes with window objectives
• Timed Basic Parallel Processes
• Reachability for bounded branching VASS
• Continuous One-counter Automata
• Equivalence checking and intersection of deterministic timed finite state machines
• Diagnosability of labeled \(\mathfrak{D}_{\mathfrak{p}}\)-automata
• Reachability in two-parametric timed automata with one parameter is EXPSPACE-complete
• Reachability for updatable timed automata made faster and more effective
• Timed games and deterministic separability
• Invariants for one-counter automata with disequality tests
• The bright side of timed opacity
• Reachability in symmetric VASS
• Reachability in vector addition system with states parameterized by geometric dimension
• A note on the parameterised complexity of coverability in vector addition systems
• On the complexity of timed pattern matching

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 Q2347796)