A Specification-Guided Framework for Temporal Logic Control of Nonlinear Systems

DOI10.1109/TAC.2022.3168489MaRDI QIDQ6053240zbMATH OpenOpenAlexFDO

Authors Yinan Li, Jun Liu

Publication date 26 September 2023

Published in IEEE Transactions on Automatic Control (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2104.01385

zbMATH Keywords

formal methodsinterval analysislinear temporal logic (LTL)nonlinear control

Mathematics Subject Classification ID

Systems theory; control (93-XX)

Abstract: This paper proposes a specification-guided framework for control of nonlinear systems with linear temporal logic (LTL) specifications. In contrast with well-known abstraction-based methods, the proposed framework directly characterizes the winning set, i.e., the set of initial conditions from which a given LTL formula can be realized, over the continuous state space of the system via a monotonic operator. Following this characterization, an algorithm is proposed to practically approximate the operator via an adaptive interval subdivision scheme, which yields a finite-memory control strategy. We show that the proposed algorithm is sound for full LTL specifications, and robustly complete for specifications recognizable by deterministic B"uchi automata (DBA), the latter in the sense that control strategies can be found whenever the given specification can be satisfied with additional bounded disturbances. Without having to compute and store the abstraction and the resulting product system with the DBA, the proposed method is more memory efficient, which is demonstrated by complexity analysis and performance tests. A pre-processing stage is also devised to reduce computational cost via a decomposition of the specification. We show that the proposed method can effectively solve real-world control problems such as jet engine compressor control and motion planning for manipulators and mobile robots.

Cited in

(9)

• Verification of N-M switching control system: a case study in temporal logic model checking
• Receding horizon control for temporal logic specifications
• Specification-guided controller synthesis for linear systems and safe linear-time temporal logic
• Abstraction, discretization, and robustness in temporal logic control of dynamical systems
• Parameter Synthesis for Piecewise Affine Systems from Temporal Logic Specifications
• Control problems in a temporal logic framework
• scientific article; zbMATH DE number 4119604 (Why is no real title available?)
• Temporal Logic Trees for Model Checking and Control Synthesis of Uncertain Discrete-Time Systems
• ABS: A formally correct software tool for space-efficient symbolic synthesis

This page was built for publication: A Specification-Guided Framework for Temporal Logic Control of Nonlinear Systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6053240)