Parity Games on Temporal Graphs
Pete Austin, Sougata Bose, Patrick Totzke
TL;DR
The paper addresses parity games on temporal graphs whose edge availability is ultimately periodic, focusing on determining winning regions under $\omega$-regular objectives. It leverages succinct representations of edge predicates via existential Presburger formulas and introduces summaries and certificates to avoid exhaustive expansions. A central result is a $PSPACE$-complete classification for parity games on periodic temporal graphs, established via a $PSPACE$ upper bound and a matching lower bound from punctual reachability on static graphs. The authors also identify a monotone fragment where, if the edge predicate is in $P$ and increases for one player and decreases for the other, the problem is solvable in polynomial time, and they extend the approach to ultimately periodic and periodically declining/improving settings with related hardness results.
Abstract
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 $ω$-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.