Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Counter-example guided inductive synthesis of control Lyapunov functions for uncertain systems

Daniele Masti, Filippo Fabiani, Giorgio Gnecco, Alberto Bemporad

TL;DR

The paper addresses robust design of a control Lyapunov function and a linear state-feedback controller for discrete-time linear systems with parametric uncertainty in a general compact set. It introduces a counter-example guided inductive synthesis (CEGIS) loop where a learner solves LMIs to propose $V(x)=x^\top P x$ and $u=Kx$, and a verifier performs Lipschitz-based global optimization to search for counter-examples over the uncertain set, guaranteeing finite-time convergence. Key contributions include (i) a novel CEGIS formulation for CLF design without convex outer-approximations, (ii) a Lipschitz-continuity result for the verifier’s objective enabling efficient global optimization, and (iii) finite-time convergence guarantees with demonstrated numerical effectiveness on polytopic and spherical uncertainty sets. The method offers a scalable, less conservative alternative to traditional robust S-procedure or SOS-based methods, with practical impact for automated control design under uncertainty.

Abstract

We propose a counter-example guided inductive synthesis (CEGIS) scheme for the design of control Lyapunov functions and associated state-feedback controllers for linear systems affected by parametric uncertainty with arbitrary shape. In the CEGIS framework, a learner iteratively proposes a candidate control Lyapunov function and a tailored controller by solving a linear matrix inequality (LMI) feasibility problem, while a verifier either falsifies the current candidate by producing a counter-example to be considered at the next iteration, or it certifies that the tentative control Lyapunov function actually enjoys such feature. We investigate the Lipschitz continuity of the objective function of the global optimization problem solved by the verifier, which is key to establish the convergence of our method in a finite number of iterations. Numerical simulations confirm the effectiveness of the proposed approach.

Counter-example guided inductive synthesis of control Lyapunov functions for uncertain systems

TL;DR

The paper addresses robust design of a control Lyapunov function and a linear state-feedback controller for discrete-time linear systems with parametric uncertainty in a general compact set. It introduces a counter-example guided inductive synthesis (CEGIS) loop where a learner solves LMIs to propose and , and a verifier performs Lipschitz-based global optimization to search for counter-examples over the uncertain set, guaranteeing finite-time convergence. Key contributions include (i) a novel CEGIS formulation for CLF design without convex outer-approximations, (ii) a Lipschitz-continuity result for the verifier’s objective enabling efficient global optimization, and (iii) finite-time convergence guarantees with demonstrated numerical effectiveness on polytopic and spherical uncertainty sets. The method offers a scalable, less conservative alternative to traditional robust S-procedure or SOS-based methods, with practical impact for automated control design under uncertainty.

Abstract

We propose a counter-example guided inductive synthesis (CEGIS) scheme for the design of control Lyapunov functions and associated state-feedback controllers for linear systems affected by parametric uncertainty with arbitrary shape. In the CEGIS framework, a learner iteratively proposes a candidate control Lyapunov function and a tailored controller by solving a linear matrix inequality (LMI) feasibility problem, while a verifier either falsifies the current candidate by producing a counter-example to be considered at the next iteration, or it certifies that the tentative control Lyapunov function actually enjoys such feature. We investigate the Lipschitz continuity of the objective function of the global optimization problem solved by the verifier, which is key to establish the convergence of our method in a finite number of iterations. Numerical simulations confirm the effectiveness of the proposed approach.
Paper Structure (13 sections, 3 theorems, 15 equations, 1 algorithm)

This paper contains 13 sections, 3 theorems, 15 equations, 1 algorithm.

Table of Contents

  1. Introduction
  2. Problem definition and preliminaries
  3. Control Lyapunov functions design through counter-examples
  4. The learner task
  5. The verifier task
  6. The proposed CEGIS scheme
  7. Computational aspects
  8. Tradeoff induced by $\eta$ and $\varepsilon$
  9. Speeding up the verification process
  10. Numerical examples
  11. Polytopic uncertainty set
  12. Spherical uncertainty set
  13. Conclusion

Key Result

Lemma 1

Consider two symmetric matrices $K$ and $L$ of the same dimension. Then, it holds that $| \lambda_{\mathrm{min}}(K)-\lambda_{\mathrm{min}}(K+L)| \leq || L||_{\mathrm{op}}$, where $|| \cdot||_{\mathrm{op}}$ is the operator norm of a matrix, induced by the $l_2$-norm. $\square$

Theorems & Definitions (8)

  • Lemma 1: hornjohnson1991
  • Theorem 1
  • proof
  • Remark 1
  • Theorem 2
  • proof
  • Remark 2
  • Remark 3