Temporal logics have garnered significant attention in the control community due to their use for formal control synthesis, namely for the synthesis of control policies with provable correctness guarantees for more complex and interesting properties than traditional control objectives. Formal control under temporal logics is fundamentally challenging though, particularly when dealing with uncertain infinite systems and complex temporal logic specifications for real-time task planing, as the established methods struggle with handling models in high dimensions and with accommodating online deployment. In this article, we propose Temporal Logic Trees (TLT) as a mitigation for these challenges. TLT are constructed from Linear Temporal Logic (LTL) formulae via reachability analysis, offering an abstraction-free design method. Building upon the TLT framework, we present approaches for adaptive task planning and formal control synthesis that are usable on both finite and infinite systems. Furthermore, we demonstrate the applicability of our approach for online control synthesis, particularly in addressing time-varying tasks: namely, our method allows for dynamic online updates of the specifications, which showcases its practical utility and flexibility.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Adaptive Task Planning and Formal Control Synthesis Using Temporal Logic Trees

  • Yulong Gao,
  • Can Zhou,
  • Alessandro Abate,
  • Karl H. Johansson

摘要

Temporal logics have garnered significant attention in the control community due to their use for formal control synthesis, namely for the synthesis of control policies with provable correctness guarantees for more complex and interesting properties than traditional control objectives. Formal control under temporal logics is fundamentally challenging though, particularly when dealing with uncertain infinite systems and complex temporal logic specifications for real-time task planing, as the established methods struggle with handling models in high dimensions and with accommodating online deployment. In this article, we propose Temporal Logic Trees (TLT) as a mitigation for these challenges. TLT are constructed from Linear Temporal Logic (LTL) formulae via reachability analysis, offering an abstraction-free design method. Building upon the TLT framework, we present approaches for adaptive task planning and formal control synthesis that are usable on both finite and infinite systems. Furthermore, we demonstrate the applicability of our approach for online control synthesis, particularly in addressing time-varying tasks: namely, our method allows for dynamic online updates of the specifications, which showcases its practical utility and flexibility.