2025/10/28 by Jamroga, Wojciech, Kurpiewski, Damian, Mikulski, Łukasz
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Multiagent Systems (cs.MA)
paper · doi:10.48550/arxiv.2511.10649
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."