Robustly Complete Synthesis of Memoryless Controllers for Nonlinear Systems with Reach-and-Stay Specifications

TL;DR

This paper introduces a finite algorithm for synthesizing memoryless controllers for nonlinear systems with reach-and-stay specifications, ensuring robustness and completeness where previous methods lacked guarantees.

Contribution

It presents a fixed-point based approach with adaptive partitioning that guarantees termination, robustness, and completeness for control synthesis in nonlinear systems.

Findings

Algorithm guarantees control strategy if specification is robustly realizable

Adaptive partitioning improves approximation accuracy and reduces computation time

Effectiveness demonstrated on multiple benchmarking examples

Abstract

This paper proposes a finitely terminating algorithm to solve reach-and-stay control problems for nonlinear systems. The algorithm is guaranteed to return a control strategy if the specification is robustly realizable. Such a feature is desirable as the commonly used abstraction-based methods are sound but not complete for systems that are not incrementally stable. Fundamental to the proposed method is a fixed-point characterization of the winning set of the system with respect to a given specification, i.e., the initial states that can be controlled to satisfy the specification. The use of an adaptive partitioning scheme not only guarantees the approximation precision of the winning set but also reduces computational time. The effectiveness and efficiency are illustrated by several benchmarking examples.