Concurrent Games in Dynamic Epistemic Logic

Concurrent Games in Dynamic Epistemic Logic

Bastien Maubert, Sophie Pinchinat, Francois Schwarzentruber, Silvia Stranieri

Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence
Main track. Pages 1877-1883. https://doi.org/10.24963/ijcai.2020/260

Action models of Dynamic Epistemic Logic (DEL) represent precisely how actions are perceived by agents. DEL has recently been used to define infinite multi-player games, and it was shown that they can be solved in some cases. However, the dynamics being defined by the classic DEL update product for individual actions, only turn-based games have been considered so far. In this work we define a concurrent DEL product, propose a mechanism to resolve conflicts between actions, and define concurrent DEL games. As in the turn-based case, the obtained concurrent infinite game arenas can be finitely represented when all actions are public, or all are propositional. Thus we identify cases where the strategic epistemic logic ATL*K can be model checked on such games.
Keywords:
Knowledge Representation and Reasoning: Reasoning about Knowledge and Belief
Planning and Scheduling: Theoretical Foundations of Planning
Agent-based and Multi-agent Systems: Formal Verification, Validation and Synthesis