Sciweavers

HYBRID
2000
Springer

Decidability and Complexity Results for Timed Automata and Semi-linear Hybrid Automata

13 years 7 months ago
Decidability and Complexity Results for Timed Automata and Semi-linear Hybrid Automata
Abstract. We define a new class of hybrid automata for which reachability is decidable--a proper superclass of the initialized rectangular hybrid automata--by taking parallel compositions of simple components. Attempting to generalize, we encounter timed automata with algebraic constants. We show that reachability is undecidable for these algebraic timed automata by simulating two-counter Minsky machines. Modifying the construction to apply to parametric timed automata, we reprove the undecidability of the emptiness problem, and then distinguish the dense and discrete-time cases with a new result. The algorithmic complexity-both classical and parametric--of one-clock parametric timed automata is also examined. We finish with a table of computability-theoretic complexity results, including that the existence of a Zeno run is 1 1-complete for semi-linear hybrid automata; it is too complex to be expressed in first-order arithmetic.
Joseph S. Miller
Added 24 Aug 2010
Updated 24 Aug 2010
Type Conference
Year 2000
Where HYBRID
Authors Joseph S. Miller
Comments (0)