Robustly complete synthesis of sampled-data control for continuous-time nonlinear systems with reach-and-stay objectives. (May 2022)

• Record Type: Journal Article
• Authors: Li, Yinan; Liu, Jun
• Is Part Of: Nonlinear analysis. Volume 44(2022)
• Publication Date: 2022-05
• Subjects: Nonlinear systems -- Formal methods in control -- Interval analysis -- Reachability analysis -- Robustness -- Completeness; Nonlinear functional analysis -- Periodicals; Analyse fonctionnelle non linéaire -- Périodiques; Nonlinear functional analysis; Periodicals; 515.7248
• DOI: 10.1016/j.nahs.2022.101170
• Languages: English
• ISSNs: 1751-570X

Abstract

Abstract: Formal methods are becoming favorable for control and verification of safety-critical systems because of the rigorous model-based computation. Relying on an over-approximated model of the original system behaviors, formal control synthesis algorithms are not often complete, which means that a controller cannot necessarily be synthesized even if there exists one. The main result of this paper shows that, for continuous-time nonlinear systems, a sample-and-hold control strategy for a reach-and-stay specification can be synthesized whenever such a strategy exists for the same system with its dynamics perturbed by small disturbances. Control synthesis is carried out by a fixed-point algorithm that adaptively partitions the system state space into a finite number of cells. In each iteration, the reachable set from each cell after one sampling time is over-approximated within a precision determined by the bound of the disturbances. To meet such a requirement, we integrate validated high-order Taylor expansion of the system solution over one sampling period into every fixed-point iteration and provide a criterion for choosing the Taylor order and the partition precision. Two nonlinear system examples are given to illustrate the effectiveness of the proposed method. Highlights: Algorithmically synthesizes sample-and-hold control strategy for nonlinear systems. Presents sound and robustly complete conditions for the proposed algorithm. Uses validated reachable set approximation to achieve robust completeness. Precisely inner-approximates regions-of-attraction for nonlinear systems.