Asynchronous Agents with Perfect Recall: Model Reductions, Knowledge-Based Construction, and Model Checking for Coalitional Strategies
Dilian Gurov, Filip Jamroga, Wojciech Jamroga, Mateusz Kamiński, Damian Kurpiewski, Wojciech Penczek, Teofil Sidoruk
TL;DR
The paper tackles the difficult problem of model checking strategic abilities for memoryful agents in asynchronous multi-agent systems. It introduces input/output concurrent game structures ($\mathrm{I/O\ iCGS}$) with a new asynchronous execution semantics, and integrates two principal approaches—partial-order reductions and knowledge-based subset construction (KBSC)—to enable practical verification of $\mathbf{ATL_{iR}}$-style specifications. It shows that KBSC expansions preserve memoryful strategic abilities in a sound but incomplete way, and it develops an on-the-fly partial-order reduction framework for $\mathrm{iR}$-strategies that preserves key temporal-epistemic properties through stuttering-equivalence and event-independence arguments. The combination yields decidable approximations and scalable verification paths for reasoning about memoryful coalitions, with potential applicability to security and cyber-attack scenarios where attackers possess substantial memory and imperfect information. Overall, the work provides a cohesive methodology to reason about memoryful strategies in asynchronous MAS, balancing theoretical guarantees with practical model-checking feasibility, and it advances the state of the art in sound-but-incomplete verification of strategic abilities.
Abstract
Model checking of strategic abilities for agents with memory is a notoriously hard problem, and very few attempts have been made to tackle it. In this paper, we present two important steps towards this goal. First, we take the partial-order reduction scheme that was recently proved to preserve individual and coalitional abilities of memoryless agents, and show that it also works for agents with memory. Secondly, we take the Knowledge-Based Subset Construction, that was recently studied for synchronous concurrent games, and adapt it to preserve abilities of memoryful agents in asynchronous MAS. On the way, we also propose a new execution semantics for strategies in asynchronous MAS, that combines elements of Concurrent Game Structures and Interleaved Interpreted Systems in a natural and intuitive way.