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 , a temporal specification and a temporal assumption , where both and are given as linear temporal logic (LTL) formulas over the vertex set of . We call the tuple an augmented game and interpret it in the classical way, i.e., winning the augmented game is equivalent to winning the (standard) game . Given a reachability or parity game and some progress assumption , this paper establishes whether solving the augmented game lies in the same complexity class as solving . 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.