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

TL;DR

This paper introduces a counter-example guided inductive synthesis (CEGIS) method for designing control Lyapunov functions and controllers for uncertain linear systems, ensuring convergence through Lipschitz continuity analysis.

Contribution

It presents a novel CEGIS framework that iteratively synthesizes control Lyapunov functions for uncertain systems using LMIs and guarantees finite convergence.

Findings

Effective synthesis of control Lyapunov functions for uncertain systems

Finite convergence of the proposed CEGIS method

Numerical simulations demonstrate practical effectiveness

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.