PV1 ⊧ RINOComputes reachable sets for dynamical systems

Application domain/field

• Neural network
• Reachability
• Neural network verification

Expected input

• Open-loop or closed loop system, can be discrete or continuous-time
• Optional: Neural network which can be used as some inputs of the closed-loop system
• Optional: Configuration file to set initial values, input, and disturbances ranges, and parameters of the analysis

Format:

• System: C++
• Neural network: format inspired by the format used by Sherlock
• Configuration file: ?

Expected output

Computes inner and outer approximations of reachable sets. Inner and outer-approximations of the projection on each component of ranges, and joint 2D and 3D inner-approximations. It also computes approximations of output ranges that are reachable robustly or adversarially w.r.t. disturbances, specified as a subset of inputs.

Internals

Uses FILIB++ library for interval computations, aaflib library for affine arithmetic and FADBAD++ library for automatic differentiation.