ABSTRACT
This chapter introduces interval analysis as a validated numerical framework for set-oriented computation. In this framework, the basis representation of sets is intervals (also referred to as hyperrectangles or boxes) in Euclidean spaces, which are Cartesian products of ordinary intervals of real numbers. A salient feature of interval analysis is to provide rigorous error bounds in such computation. Interval computation plays a fundamental role in connecting dynamical systems, which evolve in a continuous state space, with formal specifications (LTL or omega-regular properties), which are discrete in nature, for verification and control synthesis for dynamical systems. Over-approximations of the one-step forward reachable sets for dynamical systems are discussed. For discrete-time systems, interval inclusion functions are used to over-approximate such reachable sets. These inclusion functions can be constructed using different approaches, including classical interval analysis or mixed monotonicity. For continuous-time systems, three different approaches are discussed, including Lipschitz growth bounds, mixed monotonicity, and validated Taylor integration. The over-approximations are then used to compute under-approximations of controlled predecessors for both discrete-time and continuous-time dynamical systems.
