## On reachability for hybrid automata over bounded time

*Thomas Brihaye*, *Laurent Doyen*, *Gilles Geeraerts*,
*Joël
Ouaknine*, *Jean-François Raskin*, and
*James Worrell*
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.

*Proceedings of ICALP 11*, LNCS 6756, 2011. 12 pages.

PDF
© 2011
Springer-Verlag.

Imprint / Data Protection