基于鲁棒性的时间窗口时序逻辑规范综合：混合整数线性规划方法

本文将介绍一项关于时间窗口时序逻辑（TWTL）规范下离散时间线性系统控制输入综合的最新研究。TWTL是一种强大的规范语言，专为信息物理系统设计，能够紧凑地表达带有明确时间约束的顺序任务。例如，机器人可能需要“在10秒内到达A点，然后在5秒后开始移动到B点”这样的任务，TWTL可以自然地描述这类需求。

该研究基于文献[1]中为TWTL引入的定量语义（即鲁棒性），将TWTL公式的鲁棒满足编码为一组混合整数线性约束，并将综合问题转化为混合整数线性规划（MILP），目标是最大化鲁棒度。研究者证明，任何目标值为正数的可行解都能确保规范在布尔意义上的满足。

论文提出了两种综合框架：开环公式和闭环模型预测控制（MPC）公式。开环公式从初始状态开始优化整个控制序列，适用于已知初始状态的场景。而MPC公式则采用滚动时域方式，在每个时间步利用当前测量状态重新求解MILP，从而能够应对状态不确定性或扰动。MPC的一个关键创新是“任务自适应视界”，它利用TWTL确定性有限自动机（DFA）确定当前活跃的子任务，并将预测视界限制在当前任务的剩余时间窗口内，而不是整个公式的完整视界。这显著降低了每次重新求解的计算成本，使得MPC在实际应用中更加高效。

这项工作为复杂时序任务下的控制系统设计提供了强有力的工具，有望在机器人导航、自动化制造、无人驾驶等需要严格时间约束的领域发挥重要作用。未来研究方向可能包括将方法扩展到非线性系统或更复杂的逻辑规范，以及在实际硬件平台上验证其性能。