The toolbox is also capable of computing the reachable sets for hybrid systems. All implemented dynamic system classes can be used to describe the different continuous flows for the discrete system states. Further, multiple different methods for the computation of the intersections with guard sets are implemented in CORA.
CORA also participates in annual competitions in the field of formal verification of hybrid systems consisting of a wide range of benchmarks spanning industry applications to high-dimensional scalability tests:
Let us consider a bouncing ball starting at an initial height \(s_0\) with initial velocity \(v_0\) as visible in the subsequent figure, where the velocity of the ball changes instantaneously when hitting the ground. The code below shows how to model such a ball in CORA. More information can be found in Section 4.3 in the CORA manual.
Further examples can be found at ./examples/hybridDynamics on GitHub.