On Reachability for Hybrid Automata over Bounded Time

TL;DR

This paper studies the decidability of the time-bounded reachability problem in hybrid automata, showing it is decidable for rectangular automata with non-negative rates but undecidable when negative rates or diagonal constraints are introduced.

Contribution

It establishes the boundary between decidability and undecidability for time-bounded reachability in hybrid automata, focusing on rectangular systems with non-negative rates.

Findings

Decidable for rectangular hybrid automata with non-negative rates within bounded time.

Undecidable if diagonal constraints or negative rates are allowed.

Practical relevance for systems like stopwatch automata.

Abstract

This paper investigates the time-bounded version of the reachability problem for hybrid automata. This problem asks whether a given hybrid automaton can reach a given target location within T time units, where T is a constant rational value. We show that, in contrast to the classical (unbounded) reachability problem, the timed-bounded version is decidable for rectangular hybrid automata provided only non-negative rates are allowed. This class of systems is of practical interest and subsumes, among others, the class of stopwatch automata. We also show that the problem becomes undecidable if either diagonal constraints or both negative and positive rates are allowed.