非表示:
キーワード:
-
要旨:
This paper deals with the problem of safety verification of 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.
