## Time-bounded reachability for monotonic hybrid automata:
Complexity and fixed points

*Thomas Brihaye*,
*Laurent Doyen*,
*Gilles Geeraerts*
*Joël
Ouaknine*,
*Jean-François Raskin*,
and *James Worrell*
We study the *time-bounded reachability problem* for *monotonic
hybrid automata* (MHA), i.e., rectangular hybrid automata for which
the rate of each variable is either always non-negative or always
non-positive. In this paper, we revisit the decidability results
presented in [5] and show that the problem is NEXPTIME-complete. We
also show that we can effectively compute fixed points that
characterise the sets of states that are reachable
(resp. co-reachable) within *T* time units from a given state.

*Proceedings of ATVA 13*, LNCS 8172, 2013. 15 pages.

PDF
© 2013
Springer-Verlag.

Imprint / Data Protection