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

摘要: We define a new class of hybrid automata for which reachability is decidable--a proper superclass the initialized rectangular automata--by taking parallel compositions simple components. Attempting to generalize, we encounter timed with algebraic constants. show that undecidable these by simulating two-counter Minsky machines. Modifying construction apply parametric automata, reprove undecidability emptiness problem, and then distinguish dense discrete-time cases result. The algorithmic complexity-- both classical parametric--of one-clock also examined. finish table computability-theoretic complexity results, including existence Zeno run Σ11 -complete semi-linear automata; it too complex be expressed in first-order arithmetic.