A Class of Control Certificates to Ensure Reach-While-Stay for Switched Systems

TL;DR

This paper introduces a novel method for synthesizing switching controllers for systems to achieve reach-while-stay properties, combining control barrier and Lyapunov functions and solving nonlinear constraints with SMT solvers.

Contribution

It proposes a new class of control certificates that facilitate controller synthesis for reach-while-stay specifications in switched systems, using a combined barrier-Lyapunov approach.

Findings

Method is computationally feasible for complex systems.

Outperforms or complements existing tools like SCOTS.

Successfully demonstrated on numerical examples.

Abstract

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.