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

Hadi Ravanbakhsh
(University of Colorado, Boulder)
Sriram Sankaranarayanan
(University of Colorado, Boulder)

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.

In Dana Fisman and Swen Jacobs: Proceedings Sixth Workshop on Synthesis (SYNT 2017), Heidelberg, Germany, 22nd July 2017, Electronic Proceedings in Theoretical Computer Science 260, pp. 44–61.
Published: 28th November 2017.

ArXived at: http://dx.doi.org/10.4204/EPTCS.260.6 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org