Solving Two-Player Games under Progress Assumptions

Abstract

This paper considers the problem of solving infinite two-player games over finite graphs under various classes of progress assumptions motivated by applications in cyber-physical system (CPS) design. Formally, we consider a game graph G, a temporal specification $Φ$ and a temporal assumption $ψ$, where both are given as linear temporal logic (LTL) formulas over the vertex set of G. We call the tuple $(G,Φ,ψ)$ an 'augmented game' and interpret it in the classical way, i.e., winning the augmented game $(G,Φ,ψ)$ is equivalent to winning the (standard) game $(G,ψ\implies Φ)$. Given a reachability or parity game $(G,Φ)$ and some progress assumption $ψ$, this paper establishes whether solving the augmented game $(G,Φ,ψ)$ lies in the same complexity class as solving $(G,Φ)$. While the answer to this question is negative for arbitrary combinations of $Φ$ and $ψ$, a positive answer results in more efficient algorithms, in particular for large game graphs. We therefore restrict our attention to particular classes of CPS-motivated progress assumptions and establish the worst-case time complexity of the resulting augmented games. Thereby, we pave the way towards a better understanding of assumption classes that can enable the development of efficient solution algorithms in augmented two-player games.