Hybrid systems model complex dynamical systems that combine discrete and con- tinuous components. Reachability questions, regarding whether a system can run into certain subset of its state space, stand at the core of verification and synthesis problems for hybrid systems.
Successful reachability analysis methods for hybrid systems requires the unification of techniques from at least two traditions:
As concrete examples, one can observe how the two types of techniques interact in the existing approaches towards reachability analysis. Reachable set computation methods explicitly construct flow-pipes that overapproximate the reachable states over time, while efficient computation of such overapproximations requires symbolic representations such as support functions. Constraint solving methods symbolically encode reachability properties as logic formulas, while solving such formulas requires numerically-d