Asynchronous Agents with Perfect Recall: Model Reductions, Knowledge-Based Construction, and Model Checking for Coalitional Strategies

TL;DR

This paper advances model checking for agents with memory by extending partial-order reduction techniques and adapting knowledge-based constructions to asynchronous multi-agent systems, enabling more efficient verification of coalitional strategies.

Contribution

It extends partial-order reduction to memoryful agents and adapts knowledge-based subset construction for asynchronous systems, improving model checking capabilities.

Findings

Partial-order reduction preserves abilities for memoryful agents.

Knowledge-based subset construction adapted for asynchronous MAS.

New semantics for strategies in asynchronous MAS introduced.

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.