Solving Two-Player Games under Progress Assumptions
Anne-Kathrin Schmuck, K. S. Thejaswini, Irmak Sağlam, Satya Prakash Nayak
TL;DR
This work studies solving infinite two-player CPS-design games modeled as augmented games $$(G,\Phi,\psi)$$, where the environment’s progress assumption $\psi$ is given in LTL over the vertex set. It investigates whether solving augmented reachability and parity games remains in PTIME/QP for various CPS-motivated classes of progress assumptions, and shows a dichotomy: certain local, structured progress notions (e.g., live edges, co-live edges, persistent live groups) admit efficient fixed-point or quasi-polynomial algorithms, while more expressive live groups can yield NP-complete problems, particularly under product constructions. The authors provide reductions and algorithmic strategies (including nested fixed points and quasi-polynomial approaches) that clarify which assumption classes enable efficient synthesis, and they prove NP-hardness for general live groups and related CNF-formulations, as well as product-based hardness results. The results have practical implications for CPS design by identifying when augmented game formulations can be solved efficiently and when they become intractable, guiding abstraction and modeling choices in reactive synthesis for CPS. All mathematical notation is presented with explicit delimiters to ensure precise, machine-readable representations.
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.