Verifying hybrid automata through the counterexample-guided refinement of template polyhedra
Template polyhedra generalize intervals and octagons to
polyhedra whose facets are normal to arbitrary sets of directions. They
have been employed in the abstract interpretation of programs and, with
particular success, in the reachability analysis of hybrid automata.
While previously, the choice of directions has been left to the user or a
heuristic, we present a method for the automatic discovery of directions
that generalize and eliminate spurious counterexamples. We show that our
method applies to linear and nonlinear hybrid automata with constant
derivatives, and to hybrid automata with linear ODE. We embed it inside
a CEGAR loop and we demonstrate its efficacy on the time-unbounded
reachability of several benchmarks.