Inner and outer approximations of arbitrarily quantified reachability problems

We propose an approach for computing inner and outer-approximations of the sets of values that satisfy constraints expressed as arbitrarily quantified formulas. Such formulas arise for example when specifying important problems in control such as robustness, motion planning and controller comparison. We propose an interval-based method which allows for tight but tractable approximations. We demonstrate its applicability through a series of examples and benchmarks using a prototype implementation. Finally, we develop higher-order methods, particularly tractable order one methods which provide even tighter results.