Towards Assume-Guarantee Verification of Abilities in Stochastic Multi-Agent Systems
Wojciech Jamroga, Damian Kurpiewski, Łukasz Mikulski
TL;DR
This work tackles verification of strategic abilities in stochastic multi-agent systems with imperfect information by extending assume-guarantee techniques to probabilistic ATL* and introducing a novel ATL_* variant capturing "achieving at most" φ. It develops a compositional framework with sound (and partially complete) schemes for probabilistic reasoning, separates non-probabilistic outcome structure from probabilistic aggregation, and integrates strategy synthesis to avoid full global model checking. A key contribution is the introduction of a new logic for willful incompetence, widehat{ATL}, which enhances expressivity to capture weaker, non-strict enforcement properties while preserving comparable verification complexity. The results advance compositional verification of probabilistic strategic abilities under imperfect information, offering practical pathways for scalable analysis and outlining avenues for future extension to probabilistic strategies and deeper nested-operator reasoning.
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."