Time-bounded Reachability for Hybrid Automata: Complexity and Fixpoints
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.
Keywords
Cite
@article{arxiv.1211.1276,
title = {Time-bounded Reachability for Hybrid Automata: Complexity and Fixpoints},
author = {Thomas Brihaye and Laurent Doyen and Gilles Geeraerts and Joël Ouaknine and Jean-François Raskin and James Worrell},
journal= {arXiv preprint arXiv:1211.1276},
year = {2012}
}
Comments
Submitted