Towards Assume-Guarantee Verification of Abilities in Stochastic Multi-Agent Systems
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866909900987170816 |
|---|---|
| author | Jamroga, Wojciech Kurpiewski, Damian Mikulski, Łukasz |
| author_facet | Jamroga, Wojciech Kurpiewski, Damian Mikulski, Łukasz |
| contents | Model checking of strategic abilities is a notoriously hard problem, even more so in the realistic case of agents with imperfect information, acting in a stochastic environment. Assume-guarantee reasoning can be of great help here, providing a way to decompose the complex problem into a small set of easier subproblems.
In this paper, we propose several schemes for assume-guarantee verification of probabilistic alternating-time temporal logic with imperfect information. We prove the soundness of the schemes, and discuss their completeness. On the way, we also propose a new variant of (non-probabilistic) alternating-time logic, where the strategic modalities capture "achieving at most $φ$," analogous to Levesque's logic of "only knowing." |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_10649 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Towards Assume-Guarantee Verification of Abilities in Stochastic Multi-Agent Systems Jamroga, Wojciech Kurpiewski, Damian Mikulski, Łukasz Multiagent Systems Logic in Computer Science Model checking of strategic abilities is a notoriously hard problem, even more so in the realistic case of agents with imperfect information, acting in a stochastic environment. Assume-guarantee reasoning can be of great help here, providing a way to decompose the complex problem into a small set of easier subproblems. In this paper, we propose several schemes for assume-guarantee verification of probabilistic alternating-time temporal logic with imperfect information. We prove the soundness of the schemes, and discuss their completeness. On the way, we also propose a new variant of (non-probabilistic) alternating-time logic, where the strategic modalities capture "achieving at most $φ$," analogous to Levesque's logic of "only knowing." |
| title | Towards Assume-Guarantee Verification of Abilities in Stochastic Multi-Agent Systems |
| topic | Multiagent Systems Logic in Computer Science |
| url | https://arxiv.org/abs/2511.10649 |