Solving Two-Player Games under Progress Assumptions

Explore the complexities of solving infinite two-player games over finite graphs under various progress assumptions in this 19-minute conference talk from VMCAI'24. Delve into the problem of augmented games, where a game graph G, temporal specification Φ, and temporal assumption ψ are considered. Examine how winning an augmented game (G,Φ,ψ) equates to winning the standard game (G,ψ → Φ). Investigate whether solving augmented games (G,Φ,ψ) falls within the same complexity class as solving standard games (G,Φ), focusing on reachability and parity games. Analyze specific classes of progress assumptions motivated by cyber-physical system (CPS) design, and understand their impact on worst-case time complexity. Gain insights into the development of efficient solution algorithms for augmented two-player games, paving the way for advancements in CPS design and game theory.