Simulations for Multi-Agent Systems with Imperfect Information

摘要

Equivalence-checking and simulations are well-known methods used to reduce the size of a system in order to verify it more efficiently. While Alur et al. proposed a notion of simulation sound and complete for ATL as early as 1998, there have been very few works on equivalence-checking performed on extensions of ATL* with probabilities, imperfect information, counters etc. In the case of multi-agent systems (MASs) with imperfect information, the lack of sound and complete algorithm mostly follows from the undecidability of ATL model-checking. However, while ATL is undecidable overall, there exist sub-classes of MASs for which ATL becomes decidable. In this paper, we propose a notion of simulation sound for ATL/ATL* on any MASs and complete on naive MASs. Using our simulations we design an equivalence-checking algorithm sound and complete for MASs with public actions.