提出基于算子的STL新方法，解决复杂嵌套公式的验证与在线控制难题。
An Operator-based Approach to STL
- 用算子操作可达性函数，直接构建嵌套规则
- 理论证明公式满足的充要条件，支持复杂逻辑
- 适用于自动驾驶等需实时决策的系统
信号时序逻辑（STL）因其丰富的表达能力，在自主规划与控制中得到广泛应用。然而，现有验证与控制综合方法在处理复杂嵌套公式时仍受限。本文提出一种基于算子的STL新方法，该算子作用于可达性值函数，构建了全新的理论框架，可有效处理复杂多层嵌套公式，并支持在线控制合成。不同于传统设计STL可达性（或控制屏障）函数的思路，本方法直接建立算子型嵌套规则。理论层面，我们推导出STL公式满足的充要条件；仿真验证也展示了其在复杂片段上的有效性。
原文摘要 · Abstract (English)
Signal Temporal Logic (STL), has recently seen extensive development, owing to its rich expressivenes for autonomous planning and control. Nevertheless, existing verification and control synthesis methods are limited with respect to the complexity and degree of nesting of the formulae. In this work, we propose a novel approach to STL based on an operator acting on reachability value functions. This constitutes a new theoretical framework for handling complex multi-nested formulae while at the same time providing tools for on-line control synthesis. In contrast to focusing on the design of STL-based reachability (or control barrier) functions, we develop operator-based nesting rules directly. Our method's expressiveness is demonstrated both theoretically, where necessary and sufficient conditions for STL formula satisfaction are extracted, as well as in simulations with complex fragments.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。