这篇于2026年6月29日提交至arXiv的论文《Robustness-Based Synthesis for Time Window Temporal Logic Specifications via Mixed-Integer Linear Programming》（通过混合整数线性规划实现时间窗口时序逻辑规范的基于鲁棒性的综合），由Philip Smith等三位作者完成，归属于机器人学（cs.RO）与形式语言与自动机理论（cs.FL）两个学科分类，编号为arXiv:2606.30820v1，全文约293 KB。
时间窗口时序逻辑（TWTL）是一种面向信息物理系统的丰富规范语言，能够紧凑地表达带有明确时间约束的时序任务。这类规范允许工程师用形式化方式描述诸如“在某个时间窗内完成某项操作、随后在另一指定窗口内完成下一项操作”的序列任务，从而为自动控制与验证提供严格的数学基础。论文聚焦的核心问题是：如何为离散时间线性系统合成满足TWTL任务规范的控制输入。
在方法上，作者建立在近期文献[1]为TWTL引入的定量语义（即鲁棒性，robustness）之上。所谓鲁棒性，衡量的是一个轨迹在多大程度上满足给定公式——正值代表满足，数值越大表示距离违反约束越远、裕度越大。作者将TWTL公式的鲁棒满足性编码为一组混合整数线性约束，并把控制综合问题表述为一个最大化鲁棒性程度的混合整数线性规划（MILP）。论文给出了一个关键的理论保证：任何目标值为正的可行解，都必然保证规范在布尔意义下被满足。这一结论把连续优化与离散正确性联系起来，使求解器给出的数值解可以直接转化为对任务规范的严格满足。
论文讨论了两种综合设置。其一是开环（open-loop）形式，即从初始状态出发，一次性优化完整的控制序列；这种方式适合已知完整模型、无外部扰动或测量不确定性的场景。其二是闭环形式，采用滚动时域模型预测控制（MPC），在每个控制步利用当前实测状态重新求解MILP，从而对状态偏差与扰动做出在线修正。
该MPC形式的一个突出特点是“任务自适应时域”（task-adaptive horizon）。作者利用TWTL对应的确定性有限自动机（DFA）来判定每一步当前处于哪个活跃子任务，并把预测时域限制在当前任务剩余的时间窗口之内，而不是使用整个公式的完整时域。由于每一步的优化规模因此大幅缩小，每次重新求解的计算代价显著低于最初的开环全局求解，使在线闭环综合在计算上更加可行。
论文的贡献可概括为：为TWTL规范提供了一种基于鲁棒性的MILP编码与综合框架；证明了正目标值可行解蕴含布尔满足性；并设计了结合DFA驱动的任务自适应时域MPC闭环方案。这些结果面向机器人等需要严格遵守时序约束的信息物理系统，为将丰富的时序任务规范转化为可求解的优化问题提供了系统化途径。