hide
Free keywords:
-
Abstract:
This paper deals with the problem of safety verification of nonlinear 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 interval-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. Tests of such an
implementation are promising.