Counterexample Guided Synthesis of Switched Controllers for Reach-While-Stay Properties

Understand

We introduce a counter-example guided inductive synthesis (CEGIS) framework for synthesizing continuous-time switching controllers that guarantee reach while stay (RWS) properties of the closed loop system.

• The solution is based on synthesizing specially defined class of control Lyapunov functions (CLFs) for switched systems, that yield switching controllers with a guaranteed minimum dwell time in each mode.
• Next, we use a CEGIS-based approach to iteratively solve the resulting quantified exists-forall constraints, and find a CLF.
• We introduce relaxations to guarantee termination, as well as heuristics to increase convergence speed.