In this work, we propose a novel approach for the continuous-time control synthesis of nonlinear systems under nested signal temporal logic (STL) specifications. While the majority of existing literature focuses on control synthesis for STL specifications without nested temporal operators, addressing nested temporal operators poses a notably more challenging scenario and requires new theoretical advancements. Our approach hinges on the concepts of signal temporal logic tree (sTLT) and control barrier function (CBF). Specifically, we detail the construction of an sTLT from a given STL formula and a continuous-time dynamical system, the sTLT semantics (i.e., satisfaction condition), and the equivalence or under-approximation relation between sTLT and STL. Leveraging the fact that the satisfaction condition of an sTLT is essentially keeping the state within certain sets during certain time intervals, it provides explicit guidelines for the CBF design. The resulting controller is obtained through the utilization of an online CBF-based program coupled with an event-triggered scheme for online updating the activation time interval of each CBF, with which the correctness of the system behavior can be established by construction. We demonstrate the efficacy of the proposed method for single-integrator and unicycle models under nested STL formulas.

翻译：本文提出了一种针对非线性系统在嵌套信号时态逻辑（STL）规范下的连续时间控制综合新方法。现有文献主要关注不含嵌套时态算子的STL规范控制综合问题，而处理嵌套时态算子则构成了更具挑战性的场景，需要新的理论突破。我们的方法基于信号时态逻辑树（sTLT）和控制障碍函数（CBF）这两个核心概念。具体而言，我们详细阐述了如何从给定STL公式和连续时间动态系统构建sTLT，给出了sTLT的语义（即满足条件），以及sTLT与STL之间的等价或欠逼近关系。利用sTLT满足条件本质上是在特定时间区间内将系统状态约束在特定集合内的特性，这为CBF设计提供了明确的指导原则。最终通过在线CBF程序与事件触发机制相结合获得控制器，该机制用于在线更新每个CBF的激活时间区间，从而从构造层面确保系统行为的正确性。我们通过嵌套STL公式下的单积分器模型和独轮车模型验证了所提方法的有效性。