DDReach

The statistical verification for stochastic dynamical systems suffers from data-efficiency and scalability to provide probabilistic guarantees. In this technique we propose a novel combination of learning and reachability which provides us scalable tools to propose guarantees for high dimensional systems. The method incorporates conformal inference for error analyis of a trained model on collected datasets and provides a guaranteed flowpipe to cover the traces of the real system that has also distribution shift. We were abale to propose reachability for high dimensional and highly nonlinear systems like 12 dimesnional quadcopters and the toolbox is available from here.