Time-bounded Reachability for Hybrid Automata: Complexity and Fixpoints

TL;DR

This paper establishes that the time-bounded reachability problem for rectangular hybrid automata with non-negative rates is NExpTime-complete, providing a more efficient algorithm and practical methods for computing reachable state sets.

Contribution

It introduces a new NExpTime algorithm for the problem, proves its optimality with matching lower bounds, and extends results to compute fixpoints for reachable states within a time bound.

Findings

The new algorithm improves complexity bounds over previous work.

Time-bounded reachability for RHA+ is NExpTime-complete.

Practical methods for computing fixpoints of reachable states are developed.

Abstract

In this paper, we study thetime-bounded reachability problem for rectangular hybrid automata with non-negative rates (RHA+). This problem was recently shown to be decidable [Brihaye et al, ICALP11] (even though the unbounded reachability problem for even very simple classes of hybrid automata is well-known to be undecidable). However, [Brihaye et al, ICALP11] does not provide a precise characterisation of the complexity of the time-bounded reachability problem. The contribution of the present paper is threefold. First, we provide a new NExpTime algorithm to solve the timed-bounded reachability problem on RHA+. This algorithm improves on the one of [Brihaye et al, ICALP11] by at least one exponential. Second, we show that this new algorithm is optimal, by establishing a matching lower bound: time-bounded reachability for RHA+ is therefore NExpTime-complete. Third, we extend these results in a practical direction, by showing that we can effectively compute fixpoints that characterise the sets of states that are reachable (resp. co-reachable) within T time units from a given starting state.