Continuous-time control synthesis under nested signal temporal logic specifications

要約

この研究では、入れ子になった信号時相論理 (STL) 仕様に基づく非線形システムの連続時間制御合成のための新しいアプローチを提案します。
既存の文献の大部分は、ネストされた時相演算子を使用しない STL 仕様の制御合成に焦点を当てていますが、ネストされた時相演算子に対処することは、より困難なシナリオを提起し、新たな理論的進歩を必要とします。
私たちのアプローチは、信号時間論理ツリー (sTLT) と制御バリア関数 (CBF) の概念に基づいています。
具体的には、与えられた STL 式と連続時間動的システムからの sTLT の構築、sTLT のセマンティクス (つまり、満足条件)、および sTLT と STL の間の等価性または過小近似関係について詳しく説明します。
sTLT の満足条件は基本的に特定の時間間隔中に特定のセット内に状態を維持することであるという事実を利用して、CBF 設計に明示的なガイドラインを提供します。
結果として得られるコントローラーは、各 CBF のアクティブ化時間間隔をオンラインで更新するためのイベント トリガー方式と組み合わせたオンライン CBF ベースのプログラムの利用を通じて得られ、システム動作の正確性を構築によって確立できます。
ネストされた STL 式の下で、単一積分器および一輪車モデルに対する提案された方法の有効性を実証します。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google