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 $\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 ⟹\Phi )$. Given a reachability or parity game $(G,\Phi )$ and some progress assumption $\psi$, this paper establishes whether solving the augmented game $(G,\Phi ,\psi )$ lies in the same complexity class as solving $(G,\Phi )$. 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.

VMCAI 2024. arXiv admin note: text overlap with arXiv:1904.12446 by other authors

References in corpus (6)

• How to Handle Assumptions in Synthesis
• Context-triggered Abstraction-based Control Design
• Computing Adequately Permissive Assumptions for Synthesis
• A Recursive Approach to Solving Parity Games in Quasipolynomial Time
• Fast Symbolic Algorithms for Omega-Regular Games under Strong Transition Fairness
• Solving Two-Player Games under Progress Assumptions

Cited by in corpus (1)

• Solving Two-Player Games under Progress Assumptions