Solving Two-Player Games under Progress Assumptions
| Autor: | Schmuck, Anne-Kathrin, Thejaswini, K. S., Sağlam, Irmak, Nayak, Satya Prakash |
|---|---|
| Rok vydání: | 2023 |
| Předmět: | |
| Druh dokumentu: | Working Paper |
| DOI: | 10.1007/978-3-031-50524-9_10 |
| Popis: | 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 $(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. Comment: VMCAI 2024. arXiv admin note: text overlap with arXiv:1904.12446 by other authors |
| Databáze: | arXiv |
| Externí odkaz: |
|