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