基於魯棒性的時間窗口時序邏輯規範綜合：混合整數線性規劃方法

本文將介紹一項關於時間窗口時序邏輯（TWTL）規範下離散時間線性系統控制輸入綜合的最新研究。TWTL是一種強大的規範語言，專為信息物理系統設計，能夠緊湊地表達帶有明確時間約束的順序任務。例如，機器人可能需要“在10秒內到達A點，然後在5秒後開始移動到B點”這樣的任務，TWTL可以自然地描述這類需求。

該研究基於文獻[1]中為TWTL引入的定量語義（即魯棒性），將TWTL公式的魯棒滿足編碼為一組混合整數線性約束，並將綜合問題轉化為混合整數線性規劃（MILP），目標是最大化魯棒度。研究者證明，任何目標值為正數的可行解都能確保規範在布爾意義上的滿足。

論文提出了兩種綜合框架：開環公式和閉環模型預測控制（MPC）公式。開環公式從初始狀態開始優化整個控制序列，適用於已知初始狀態的場景。而MPC公式則採用滾動時域方式，在每個時間步利用當前測量狀態重新求解MILP，從而能夠應對狀態不確定性或擾動。MPC的一個關鍵創新是“任務自適應視界”，它利用TWTL確定性有限自動機（DFA）確定當前活躍的子任務，並將預測視界限制在當前任務的剩餘時間窗口內，而不是整個公式的完整視界。這顯著降低了每次重新求解的計算成本，使得MPC在實際應用中更加高效。

這項工作為複雜時序任務下的控制系統設計提供了強有力的工具，有望在機器人導航、自動化製造、無人駕駛等需要嚴格時間約束的領域發揮重要作用。未來研究方向可能包括將方法擴展到非線性系統或更復雜的邏輯規範，以及在實際硬件平台上驗證其性能。