混合整数線形計画法による時間窓時相論理仕様のロバスト性に基づく合成

本論文では、時間窓時相論理（TWTL）仕様に従う離散時間線形システムの制御入力合成を扱う。TWTLは、サイバーフィジカルシステム向けの豊かな仕様言語であり、明示的な時間制約を持つ逐次タスクをコンパクトに表現できる。例えば、ロボットが「10秒以内に地点Aに到着し、その後5秒後に地点Bへの移動を開始する」といったタスクを自然に記述できる。

著者らは、TWTLに対して最近導入された定量的意味論（ロバスト性）に基づき、TWTL式のロバストな充足を混合整数線形制約としてエンコードし、合成問題をロバスト度を最大化する混合整数線形計画（MILP）として定式化する。彼らは、正の目的値を持つ任意の実行可能解が仕様のブール充足を保証することを証明した。

論文では2つの合成設定を提案している。開ループ形式は初期状態から全制御系列を最適化する。一方、閉ループ形式はモデル予測制御（MPC）を用い、各ステップで現在の測定状態に基づいてMILPを再求解する。MPC形式の重要な特徴は「タスク適応型ホライゾン」である。これはTWTL決定性有限オートマトン（DFA）を利用して各ステップでアクティブなサブタスクを特定し、予測ホライゾンを現在のタスクの残り時間窓に制限する。これにより、各再求解の計算コストは初期の開ループ求解よりも大幅に低減される。

この研究は、複雑な時間制約を持つ制御システムの合成に対して実用的なアプローチを提供し、ロボット工学、自動化、自動運転などの分野での応用が期待される。今後の課題として、非線形システムへの拡張や、実際のハードウェアでの検証が挙げられる。