Quantifying the Satisfaction of Spatio-Temporal Logic Specifications for Multiagent Control

• 成果类型: Article
• 署名作者: Liu, Wenliang; Alsalehi, Suhail; Mehdipour, Noushin; Bartocci, Ezio; Belta, Calin
• 署名单位: Boston University; Boston University; Technische Universitat Wien; University System of Maryland; University of Maryland College Park; University System of Maryland; University of Maryland College Park
• 刊物名称: IEEE TRANSACTIONS ON AUTOMATIC CONTROL
• ISSN/ISSBN: 0018-9286
• DOI: 10.1109/TAC.2025.3538747
• 发表日期: 2025
• 页码: 5098-5113
• 关键词: robustness; logic; optimization; measurement; training; Imitation learning; trajectory; semantics; Robot kinematics; Recurrent neural networks; Control system synthesis; Formal languages; Machine Learning; Multi-agent systems

摘要

In this article, we study control synthesis problems for multiagent systems (MASs) that must comply with spatio-temporal logic requirements. We define a logic called team spatio-temporal reach and escape logic (t-STREL) and a robustness metric for it that is continuous everywhere and differentiable almost everywhere. These properties facilitate the use of gradient-based optimization and learning-based control techniques, offering greater efficiency compared to traditional gradient-free methods. We propose three approaches leveraging these robustness properties to control the MAS. The first combines a gradient-based optimization algorithm with a heuristic one (hybrid optimization). The second uses imitation learning to learn a recurrent neural network (RNN) controller from a dataset generated by off-line optimizations. The third approach employs a model-based policy search algorithm to learn an RNN controller directly without a dataset. We showcase our proposed approaches in a simulated example. We demonstrate that, with hybrid optimization, the MAS can achieve a high success rate of compliance with the t-STREL requirement, while the imitation learning approach can be used for real-time control. The model-based policy search approach can concurrently achieve both objectives within a relatively short training time.