2015/09/11 by Hadi Ravanbakhsh, Ravanbakhsh, Hadi, Sriram Sankaranarayanan +1 · 2 citations
Computer Science · #Embedded Systems Design Techniques #FOS: Electrical engineering #Formal Methods in Verification #Parallel Computing and Optimization Techniques #Systems and Control (eess.SY) #electronic engineering #information engineering
paper · pdf · doi:10.48550/arxiv.1509.03688
openalex publication_date 2015/09/11 · openalex created_date 2022/10/01 · openalex updated_date 2026/07/28
We investigate the problem of synthesizing switching controllers for\nstabilizing continuous-time plants. First, we introduce a class of control\nLyapunov functions (CLFs) for switched systems along with a switching strategy\nthat yields a closed loop system with a guaranteed minimum dwell time in each\nswitching mode. However, the challenge lies in automatically synthesizing\nappropriate CLFs. Assuming a given fixed form for the CLF with unknown\ncoefficients, we derive quantified nonlinear constraints whose feasible\nsolutions (if any) correspond to CLFs for the original system. However, solving\nquantified nonlinear constraints pose a challenge to most LMI/BMI-based\nrelaxations. Therefore, we investigate a general approach called\nCounter-Example Guided Inductive Synthesis (CEGIS), that has been widely used\nin the emerging area of automatic program synthesis. We show how a LMI-based\nrelaxation can be formulated within the CEGIS framework for synthesizing CLFs.\nWe also evaluate our approach on a number of interesting benchmarks, and\ncompare the performance of the new approach with our previous work that uses\noff-the-shelf nonlinear constraint solvers instead of the LMI relaxation. The\nresults shows synthesizing CLFs by using LMI solvers inside a CEGIS framework\ncan be a computational feasible approach to synthesizing CLFs.\n