Counter-Example Guided Synthesis of Control Lyapunov Functions for Switched Systems

TL;DR

This paper presents a novel approach combining Counter-Example Guided Inductive Synthesis (CEGIS) with LMI relaxations to automatically synthesize control Lyapunov functions for stabilizing switched systems, improving computational feasibility.

Contribution

It introduces a CEGIS-based framework with LMI relaxations for synthesizing CLFs, addressing the challenge of solving nonlinear constraints in switched system control.

Findings

LMI-based CEGIS approach is computationally feasible.

The method outperforms previous nonlinear constraint solvers.

Successful application on various benchmark systems.

Abstract

We investigate the problem of synthesizing switching controllers for stabilizing continuous-time plants. First, we introduce a class of control Lyapunov functions (CLFs) for switched systems along with a switching strategy that yields a closed loop system with a guaranteed minimum dwell time in each switching mode. However, the challenge lies in automatically synthesizing appropriate CLFs. Assuming a given fixed form for the CLF with unknown coefficients, we derive quantified nonlinear constraints whose feasible solutions (if any) correspond to CLFs for the original system. However, solving quantified nonlinear constraints pose a challenge to most LMI/BMI-based relaxations. Therefore, we investigate a general approach called Counter-Example Guided Inductive Synthesis (CEGIS), that has been widely used in the emerging area of automatic program synthesis. We show how a LMI-based relaxation can be formulated within the CEGIS framework for synthesizing CLFs. We also evaluate our approach on a number of interesting benchmarks, and compare the performance of the new approach with our previous work that uses off-the-shelf nonlinear constraint solvers instead of the LMI relaxation. The results shows synthesizing CLFs by using LMI solvers inside a CEGIS framework can be a computational feasible approach to synthesizing CLFs.