Time-Bounded Reachability for Monotonic Hybrid Automata: Complexity and Fixed Points?

Abstract. We study the time-bounded reachability problem for monotonic hy-brid 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.