Safety Verification of Hybrid Systems by Constraint Propagation Based Abstraction Refinement

non-linear hybrid systems. We start from a classical method that
uses interval arithmetic to check whether trajectories can move
over the boundaries in a rectangular grid. We put this method into
an abstraction refinement framework and improve it by developing
an additional refinement step that employs constraint propagation
to add information to the abstraction without introducing new
grid elements. Moreover, the resulting method allows switching
conditions, initial states and unsafe states to be described
by complex constraints instead of sets that correspond to grid
elements. Nevertheless, the method can be easily implemented since
it is based on a well-defined set of constraints, on which one can
run any constraint propagation based solver. First tests of such
an implementation are promising.