  In this article, we consider the problem of synthesizing switching
controllers for temporal properties through the composition of simple primitive
reach-while-stay (RWS) properties. Reach-while-stay properties specify that the
system states starting from an initial set I, must reach a goal (target) set G
in finite time, while remaining inside a safe set S. Our approach synthesizes
switched controllers that select between finitely many modes to satisfy the
given RWS specification. To do so, we consider control certificates, which are
Lyapunov-like functions that represent control strategies to achieve the
desired specification. However, for RWS problems, a control Lyapunov-like
function is often hard to synthesize in a simple polynomial form. Therefore, we
combine control barrier and Lyapunov functions with an additional compatibility
condition between them. Using this approach, the controller synthesis problem
reduces to one of solving quantified nonlinear constrained problems that are
handled using a combination of SMT solvers. The synthesis of controllers is
demonstrated through a set of interesting numerical examples drawn from the
related work, and compared with the state-of-the-art tool SCOTS. Our evaluation
suggests that our approach is computationally feasible, and adds to the growing
body of formal approaches to controller synthesis.
