時間窓時相論理（Time Window Temporal Logic, TWTL）はサイバーフィジカルシステム向けの表現力豊かな仕様記述言語であり、明示的な時間制約を伴う逐次タスクを簡潔に表現できる。本論文は、TWTLのタスク仕様が与えられた離散時間線形システムに対して制御入力を合成する問題を扱う。著者らは最近導入されたTWTLの定量的意味論（ロバスト性）に基づき、TWTL式のロバストな充足を混合整数線形制約の集合としてエンコードし、ロバスト度を最大化する混合整数線形計画問題（MILP）として合成問題を定式化する。これにより、仕様を満たす制御入力の探索を数理最適化問題として扱うことが可能になる。
著者らは、目的関数値が正となる任意の実行可能解が仕様のブール充足を保証することを証明している。この性質は、数値最適化の結果が仕様の論理的な充足に直結することを意味し、合成手法の正当性を支える重要な理論的保証である。すなわち、ロバスト度が正であれば、TWTL式は真となり、タイミング制約を含むタスクが確実に達成される。
本論文では2つの合成設定を扱う。第一は開ループ定式化であり、初期状態から全制御系列を最適化する。第二は閉ループのリセッディングホライズン模型予測制御（MPC）定式化であり、各ステップで現在の測定状態を用いてMILPを再求解する。MPC定式化の重要な特徴は、TWTLの決定性有限オートマトン（DFA）を利用して各ステップでアクティブなサブタスクを判定し、予測ホライズンを現在のタスクの残り窓に限定する「タスク適応型ホライズン」である。これにより、各再求解は初期の開ループ求解よりも大幅に安価になる。この工夫は、計算資源が限られる実システムへの適用を視野に入れた実践的な貢献である。
本論文はロボティクス（cs.RO）および形式言語とオートマトン理論（cs.FL）の分野に属し、2026年6月29日にarXivに投稿された（arXiv:2606.30820v1）。著者はPhilip Smithら3名である。提案手法は、時間制約付きの複雑なタスクをロバストに達成する制御器設計への応用が期待される。