Simulations for Multi-Agent Systems with Imperfect Information

                        Patrick Gardy and Yuxin Deng


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.