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$,且对一方玩家单调递增、对另一方单调递减,那么求解博弈的复杂度仅比静态图呈多项式增长。