Safety Verification of Implicitly Defined MPC Feedback Laws

    •  Holaza, J.; Takacs, B.; Kvasnica, M.; Di Cairano, S., "Safety Verification of Implicitly Defined MPC Feedback Laws", European Control Conference (ECC), DOI: 10.1109/ECC.2015.7330921, July 2015, pp. 2547-2552.
      BibTeX Download PDF
      • @inproceedings{Holaza2015jul,
      • author = {Holaza, J. and Takacs, B. and Kvasnica, M. and {Di Cairano}, S.},
      • title = {Safety Verification of Implicitly Defined MPC Feedback Laws},
      • booktitle = {European Control Conference (ECC)},
      • year = 2015,
      • pages = {2547--2552},
      • month = jul,
      • doi = {10.1109/ECC.2015.7330921},
      • url = {}
      • }
  • MERL Contact:
  • Research Area:


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.