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

arXiv: https://arxiv.org/abs/1505.01180 · HTML: https://mlsanity.com/paper/1505.01180/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 5 May 2015.

## Built on by (most cited first, 4 of 4)

- [Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models](https://mlsanity.com/paper/2311.09793/) (2023)
- [A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis](https://mlsanity.com/paper/2309.06090/) (2023)
- [Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial](https://mlsanity.com/paper/2605.26577/) (2026)
- [Certifying Almost-Sure Reachability in Unknown MDPs](https://mlsanity.com/paper/2610.18119/) (2026)

## Abstract (arXiv)

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. Finally, we evaluate our approach on a set of benchmarks ranging from two to six state variables. Our evaluation includes a preliminary comparison with related tools. The proposed approach shows the promise of nonlinear SMT solvers for the synthesis of provably correct switching control laws.