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 $\Phi$ and a temporal assumption $\psi$, where both are given as linear temporal logic (LTL) formulas over the vertex set of G. We call the tuple $(G,\Phi,\psi)$ an ‘augmented game’ and interpret it in the classical way, i.e., winning the augmented game $(G,\Phi,\psi)$ is equivalent to winning the (standard) game $(G,\psi \implies \Phi)$.

Given a reachability or parity game $\mathcal{G}= (G,\Phi)$ and some progress assumption $\psi$, this paper establishes whether solving the augmented game $\mathfrak{G}=(G,\Phi,\psi)$ lies in the same complexity class as solving $\mathcal{G}$. While the answer to this question is negative for arbitrary combinations of $\Phi$ and $\psi$, 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.