Temporal graphs are a popular modelling mechanism for dynamic complex systems that extend ordinary graphs with discrete time. Simply put, time progresses one unit per step and the availability of edges can change with time. We consider the complexity of solving $\omega$-regular games played on temporal graphs where the edge availability is ultimately periodic and fixed a priori. We show that solving parity games on temporal graphs is decidable in PSPACE, only assuming the edge predicate itself is in PSPACE. A matching lower bound already holds for what we call punctual reachability games on static graphs, where one player wants to reach the target at a given, binary encoded, point in time. We further study syntactic restrictions that imply more efficient procedures. In particular, if the edge predicate is in $P$ and is monotonically increasing for one player and decreasing for the other, then the complexity of solving games is only polynomially increased compared to static graphs.
翻译:时间图是一种扩展了普通图与离散时间的动态复杂系统建模机制。简而言之,时间每步推进一个单位,边的可用性随时间变化。我们研究了在时间图上求解$\omega$-正则博弈的复杂度问题,其中边的可用性具有最终周期性且预先固定。我们证明,在仅假设边谓词本身属于PSPACE的前提下,时间图上的奇偶博弈可判定且属于PSPACE。针对静态图上的所谓“准时可达性博弈”(一方玩家需在给定二进制编码时间点到达目标),已存在匹配的下界。我们进一步研究了可推导出更高效算法的语法限制条件。特别地,若边谓词属于$P$且对一方玩家单调递增、对另一方单调递减,则博弈求解的复杂度相比静态图仅呈多项式增长。