具有有界窗口奇偶性目标的时间博弈

窗口机制由Chatterjee等人为图上的二人轮流博弈中的平均收益与总收益目标引入，利用时间界限细化长期目标。该机制已在多种环境中被证明有用，最近更应用于时间系统。在时间设定中，所谓固定时间窗口奇偶性目标已被研究。固定时间窗口奇偶性目标相对于某时间界限定义，并要求在所有时刻我们都能观测到一个时间帧，即一个小于固定界限的窗口，其中最小优先级为偶数。本工作中，我们关注有界时间窗口奇偶性目标。若存在某界限使固定目标被满足，则该目标被满足。与固定目标不同，有界目标的满足对约束中出现的常数等建模选择具有鲁棒性，因为对于给定界限，常数的选择可能影响固定目标的满足。我们展示了时间自动机中有界时间窗口目标的验证可在多项式空间内执行，且带有这些目标的时间博弈可在指数时间内求解，即便对于多目标扩展亦然。这与固定情形的复杂度类相匹配。我们还提供了不同变体窗口奇偶性目标的比较。