Reachability Analysis
Reachable set of a Van der Pol oscillator
Reachable set of a bouncing ball
Reachable set of a neural network controlled car.
Various geometric set representations and set operations are used to compute the reachable sets.
Reachability analysis computes the set of states reachable under a set of conditions: The initial state is uncertain in a given range of values, the control inputs may be chosen from a set of potential values, the disturbances are bounded by a set, and parameters may also be uncertain within a certain range of values. Our research aims to develop algorithms that compute tight inner and outer approximations of forward and backward reachable sets.
Research questions include
- How can the reachable set for a specific dynamical system class be computed?
- What is the approximation error of the computed reachable set?
- How can we verify temporal-logic specifications using reachable sets?
- How can we bound the output of different classes of neural networks?
These algorithms constitute the theoretical basis for the applications in autonomous vehicles, robotics, and power systems. Our research in reachability analysis is implemented in our toolbox CORA.