Control of Nonlinear Systems with Reach-Avoid-Stay Specifications: A Lyapunov-Barrier Approach with an Application to the Moore-Greizer Model

The study of control synthesis for reach-avoid-stay objectives for nonlinear systems has received considerable interest in recent years. Such objectives can be naturally treated as a formal specification and effectively handled by formal methods. While formal methods often rely on constructing a finite-state approximation and developing algorithms to capture the winning set (a set of initial states from which a controller exists to realize the given task), Lyapunov methods can characterize stability and safety properties without having to discretize the state space. Inspired by recent work on converse Lyapunov-barrier theorems, we propose control Lyapunov-barrier functions to provide sufficient conditions for control synthesis with reach-avoid-stay specifications. A comparison between the proposed Lyapunov method and formal methods based on a fixed-point algorithm is illustrated by an application to enhancing the performance of jet engine compressors, which is based on a reduced Moore-Greitzer nonlinear ODE model. We apply a quadratic programming (QP) framework to reactively synthesize controllers in the case study.