AROC

The Automated Reachset Optimal Control (AROC) toolbox automatically constructs formally verified controllers for solving reach-avoid problems using reachability analysis. The toolbox considers general nonlinear systems with disturbances and input constraints. AROC is implemented in MATLAB, and the CORA toolbox is used to calculate reachable sets.

Main features:

• Motion Primitive Based Control: Optimal controllers for many motion primitives are synthesized offline and then applied for online control using a maneuver automaton.
• Model Predictive Control: The controller is constructed and verified at runtime, where the computation time required for the optimization based construction of the controller as well as the verification with reachability analysis are explicitly considered by the algorithm.
• Motion Planning using Maneuver Automata: Online control using the motion primitives constructed offline; interfaces to CommonRoad and CommonOcean.
• Safe Terminal Regions: Algorithms for constructing controllers that stabilize a system around a given equilibrium point and aim to maximize the size of the corresponding safe terminal region.
• Conformant Synthesis: Generation of over-approximative models that enclose all possible behaviors of the real system.