{"ID":2849196,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2511.10649","arxiv_id":"2511.10649","title":"Towards Assume-Guarantee Verification of Abilities in Stochastic Multi-Agent Systems","abstract":"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 $\\varphi$,\" analogous to Levesque's logic of \"only knowing.\"","short_abstract":"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....","url_abs":"https://arxiv.org/abs/2511.10649","url_pdf":"https://arxiv.org/pdf/2511.10649v1","authors":"[\"Wojciech Jamroga\",\"Damian Kurpiewski\",\"Łukasz Mikulski\"]","published":"2025-10-28T15:56:10Z","proceeding":"cs.MA","tasks":"[\"cs.MA\",\"cs.LO\"]","methods":"[]","has_code":false}