A Counter-Example Guided Framework for Robust Synthesis of Switched Systems Using Control Certificates
For control theorists and engineers, this work provides a formal, automated method for synthesizing switching controllers with safety and stability guarantees, though it is an incremental extension of existing CEGIS techniques.
The paper extends Counterexample Guided Inductive Synthesis (CEGIS) to synthesize control certificates (barrier/Lyapunov functions) for switched systems, enabling automatic controller synthesis for richer specifications like reach-while-stay with obstacles and control under disturbances. The approach handles nonpolynomial dynamics and is demonstrated on several examples, showing computational feasibility.
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.