A Counter-Example Guided Framework for Robust Synthesis of Switched Systems Using Control Certificates

TL;DR

This paper presents a formal, automated framework for synthesizing robust switching controllers using control certificates, extending CEGIS with SMT solvers to handle complex specifications and nonpolynomial dynamics.

Contribution

It introduces a counterexample guided synthesis method for control certificates, enabling automatic, formal controller synthesis for complex switched systems with robustness considerations.

Findings

Successfully handles systems with nonpolynomial dynamics

Demonstrates feasibility on complex examples

Extends CEGIS to richer specifications

Abstract

In this article, the problem of synthesizing switching controllers is considered through the synthesis of a "control certificate". Control certificates include control barrier and Lyapunov functions, which represent control strategies, and allow for automatic controller synthesis. Our approach encodes the controller synthesis problem as quantified nonlinear constraints. We extend an approach called Counterexample Guided Inductive Synthesis (CEGIS), originally proposed for program synthesis problems, to solve the resulting constraints. The CEGIS procedure involves the use of satisfiability-modulo theory (SMT) solvers to automate the problem of synthesizing control certificates. In this paper, we examine generalizations of CEGIS to attempt a richer class of specifications, including reach-while-stay with obstacles and control under disturbances. We demonstrate the ability of our approach to handle systems with nonpolynomial dynamics as well. The abilities of our general framework are demonstrated through a set of interesting examples. Our evaluation suggests that our approach is computationally feasible, and adds to the growing body of formal approaches to controller synthesis.