Zonotope-based Symbolic Controller Synthesis for Linear Temporal Logic Specifications

要約

この論文では、ゾノトープ技術を使用した線形時相論理 (LTL) 仕様の下での非線形制御システムのコントローラー合成問題を研究します。
ローカルからグローバルへの制御戦略は、LTL 式として表現される所望の仕様に対して提案されます。
まず、状態空間を有限のゾノトープと制約されたゾノトープに分割するための新しいアプローチが開発されます。これらはセルと呼ばれ、隣接するセルと交差することができます。
次に、交差関係からすべてのセル間のグラフを生成し、LTL 式の受け入れパスの実現を検証します。
実現検証により、制御設計が必要かどうかが判断され、有限のローカル LTL 式が得られます。
第三に、受け入れパスが実現されると、コントローラー設計のための新しい抽象化ベースの方法が導出されます。
特に、実現検証からのセルにのみ焦点を当て、ゾノトープの特性を利用して各セルを近似します。
ローカルシンボリックモデルとローカルLTL式に基づいて、すべてのローカル抽象コントローラを設計するための反復合成アルゴリズムが提案され、その存在と組み合わせによりLTL式のグローバルコントローラが確立されます。
最後に、提案されたフレームワークを移動ロボットの経路計画問題を通じて説明します。

要約(オリジナル)

This paper studies the controller synthesis problem for nonlinear control systems under linear temporal logic (LTL) specifications using zonotope techniques. A local-to-global control strategy is proposed for the desired specification expressed as an LTL formula. First, a novel approach is developed to divide the state space into finite zonotopes and constrained zonotopes, which are called cells and allowed to intersect with the neighbor cells. Second, from the intersection relation, a graph among all cells is generated to verify the realization of the accepting path for the LTL formula. The realization verification determines if there is a need for the control design, and also results in finite local LTL formulas. Third, once the accepting path is realized, a novel abstraction-based method is derived for the controller design. In particular, we only focus on the cells from the realization verification and approximate each cell thanks to properties of zonotopes. Based on local symbolic models and local LTL formulas, an iterative synthesis algorithm is proposed to design all local abstract controllers, whose existence and combination establish the global controller for the LTL formula. Finally, the proposed framework is illustrated via a path planning problem of mobile robots.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google