时光飞逝如观窗外：带窗口奇偶目标的 timed games

窗口机制由 Chatterjee 等人引入，用以在图上的二人轮流博弈中强化带时间界限的 mean-payoff 与 total-payoff 目标。此后该机制已被证明在多种场景中有用，包括博弈中的奇偶目标以及马尔可夫决策过程中的 mean-payoff 与奇偶目标。我们研究 timed automata 与 timed games 中的窗口奇偶目标：给定窗口大小界限，若路径上所有状态中均存在一个足够小的窗口使得其中最小优先级为偶数，则该路径满足此类目标。我们证明，检验 timed automaton 的所有时间发散路径是否满足此类窗口奇偶目标可在多项式空间内完成，且相应的 timed games 可在指数时间内求解。这与 timed parity games 的复杂度类一致，同时增添了推理时间界限的能力。我们还考虑了多维目标并证明复杂度类不会升高。据我们所知，这是首次在实时环境中对窗口机制的研究。