KNOWLEDGE ACQUISITION IN MULTI-AGENT SYSTEMS: A FORMALIZATION OF THE ELEUSIS CARD GAME

We deal with logical approaches to knowledge acquisition in multi-agent systems. We enhance previous work by considering the inductive card game Eleusis where dynamic knowledge about the behavior of other agents or environment, rather than traditional static knowledge about system states is acquired. Our main contributions are as follows: (1) we formalize the knowledge acquisition process in the infinite version of the Eleusis game with perfect recall (i.e., the agents never forget the acquired information), using the propositional logic of knowledge and branching time Act-CTL-K \(_n\) ${}_n$ , and (2) we formally prove that the Eleusis system with perfect recall is well structured, which in practice enables applying the recently implemented model checking methods for infinite well-structured systems. In addition to the theoretical interest, our work is also motivated by potential application fields, including cryptography.