Model Checking Multi-Agent Systems against LDLK Specifications

Model Checking Multi-Agent Systems against LDLK Specifications

Jeremy Kong, Alessio Lomuscio

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence
Main track. Pages 1138-1144. https://doi.org/10.24963/ijcai.2017/158

We define the logic LDLK, a formalism for specifying multi-agent systems. LDLK extends LDL with epistemic modalities, including common knowledge, for reasoning about the evolution of knowledge states of the agents in the system. We study the complexity of verifying a multi-agent system against LDLK specifications and show this to be in PSPACE. We give an algorithm for the practical verification of multi-agent systems specified in LDLK. We show that the model checking algorithm, based on alternating-automata and nFA, is amenable to symbolic implementation on OBDDs. We introduce MCMAS LDLK , an extension of the open-source model checker MCMAS, implementing the algorithm and discuss the experimental results obtained.
Keywords:
Knowledge Representation, Reasoning, and Logic: Logics for Knowledge Representation
Agent-based and Multi-agent Systems: Formal verification, validation and synthesis
Multidisciplinary Topics and Applications: Validation and Verification