Safety verification of implicitly defined MPC feedback laws

For a closed-loop system composed of a linear controlled plant and an MPC feedback strategy we show how to verify that closed-loop state trajectories either enter or avoid a given set of unsafe states. The search for the safety certificate is formulated as a mixed-integer linear programming problem which yields non-conservative certificates. The optimal control commands generated by the MPC policy are represented by Karush-Kuhn-Tucker optimality conditions, which allow to perform the verification without the need to explicitly compute reachable sets.