The method for verification of hybrid systems by constraint propagation based abstraction refinement that we introduced in
an earlier paper is based on an over-approximation of continuous reachability information of ordinary differential equations
using constraints that do not contain differentiation symbols. The method uses an interval constraint propagation based solver
to solve these constraints. This has the advantage that—without complicated algorithmic changes—the method can be improved
by just changing these constraints. In this paper, we discuss various possibilities of such changes, we prove some properties
about the amount of over-approximations introduced by the new constraints, and provide some timings that document the resulting
improvement.
This work was partly supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center
“Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS). See www.avacs.org for more information.