Computing Adequately Permissive Assumptions for Synthesis
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2023
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866917570938929152 |
|---|---|
| author | Anand, Ashwani Mallik, Kaushik Nayak, Satya Prakash Schmuck, Anne-Kathrin |
| author_facet | Anand, Ashwani Mallik, Kaushik Nayak, Satya Prakash Schmuck, Anne-Kathrin |
| contents | We solve the problem of automatically computing a new class of environment assumptions in two-player turn-based finite graph games which characterize an ``adequate cooperation'' needed from the environment to allow the system player to win. Given an $ω$-regular winning condition $Φ$ for the system player, we compute an $ω$-regular assumption $Ψ$ for the environment player, such that (i) every environment strategy compliant with $Ψ$ allows the system to fulfill $Φ$ (sufficiency), (ii) $Ψ$ can be fulfilled by the environment for every strategy of the system (implementability), and (iii) $Ψ$ does not prevent any cooperative strategy choice (permissiveness).
For parity games, which are canonical representations of $ω$-regular games, we present a polynomial-time algorithm for the symbolic computation of adequately permissive assumptions and show that our algorithm runs faster and produces better assumptions than existing approaches -- both theoretically and empirically. To the best of our knowledge, for $ω$-regular games, we provide the first algorithm to compute sufficient and implementable environment assumptions that are also permissive. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2301_07563 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Computing Adequately Permissive Assumptions for Synthesis Anand, Ashwani Mallik, Kaushik Nayak, Satya Prakash Schmuck, Anne-Kathrin Computer Science and Game Theory We solve the problem of automatically computing a new class of environment assumptions in two-player turn-based finite graph games which characterize an ``adequate cooperation'' needed from the environment to allow the system player to win. Given an $ω$-regular winning condition $Φ$ for the system player, we compute an $ω$-regular assumption $Ψ$ for the environment player, such that (i) every environment strategy compliant with $Ψ$ allows the system to fulfill $Φ$ (sufficiency), (ii) $Ψ$ can be fulfilled by the environment for every strategy of the system (implementability), and (iii) $Ψ$ does not prevent any cooperative strategy choice (permissiveness). For parity games, which are canonical representations of $ω$-regular games, we present a polynomial-time algorithm for the symbolic computation of adequately permissive assumptions and show that our algorithm runs faster and produces better assumptions than existing approaches -- both theoretically and empirically. To the best of our knowledge, for $ω$-regular games, we provide the first algorithm to compute sufficient and implementable environment assumptions that are also permissive. |
| title | Computing Adequately Permissive Assumptions for Synthesis |
| topic | Computer Science and Game Theory |
| url | https://arxiv.org/abs/2301.07563 |