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.