Memory Efficient Symbolic Solution Of Quantitative Reach-Avoid Problems

ion-based controller synthesis is an emerging approach to automatically synthesize correct-by-design controllers for a wide class of continuous-state control problems. Its application is currently limited, however, since the number of transitions of non-deterministic discrete abstractions for a state-input pair is exponential in dimension of the state space. In this paper, we present a novel synthesis algorithm for quantitative reach-avoid problems that does not require pre-computation of abstraction or any part of it. Our approach outperforms existing on-the-fly works by the fact that, regardless of the state space dimension, it provably stores at most one transition for any abstract state-input pair at any point in time. Hence, memory-wise, one of "bottlenecks" of abstraction-based control is removed. To achieve reasonable time complexity, we place assumptions only on the geometry of the problem data. We illustrate performance of our method on several examples.