The Hybrid I/O-automaton (HIOA) is a rigorous formal model designed for the analysis of complex hybrid (discrete-continuous) dynamical sy
Recently, efficient reachability algorithms for hybrid systems with piecewise affine dynamics have been developed.
We present a scalable reachability algorithm for hybrid systems with piecewise affine, non-deterministic dynamics.
The verification of continuous and hybrid systems is known to be hard, and today tools are limited to relatively small problems.