TY - GEN
T1 - Simulations for Multi-Agent Systems with Imperfect Information
AU - Gardy, Patrick
AU - Deng, Yuxin
N1 - Publisher Copyright:
© 2019, Springer Nature Switzerland AG.
PY - 2019
Y1 - 2019
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/85076148858
U2 - 10.1007/978-3-030-32409-4_9
DO - 10.1007/978-3-030-32409-4_9
M3 - 会议稿件
AN - SCOPUS:85076148858
SN - 9783030324087
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 138
EP - 153
BT - Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings
A2 - Ait-Ameur, Yamine
A2 - Qin, Shengchao
PB - Springer
T2 - 21st International Conference on Formal Engineering Methods, ICFEM 2019
Y2 - 5 November 2019 through 9 November 2019
ER -