An abstraction and refinement computational approach to safety verification of discrete time nonlinear systems

This paper addresses safety verification of nonlinear systems through invariant set computation. More precisely, our goal is verifying if the state of a given discrete time nonlinear system will keep evolving within a safe region, starting from a given set of initial conditions. To this purpose, we introduce a conformant PieceWise Affine (PWA) abstraction of the nonlinear system, which is instrumental to computing a conservative approximation of its maximal invariant set within the safe region. If the obtained set covers the set of initial conditions, safety is proven. Otherwise, subsequent refinements of the PWA abstraction are performed, either on the whole safe region or on some appropriate subset identified through a guided refinement approach and containing the set of initial conditions. Some numerical examples demonstrate the effectiveness of the approach.