Model Checking Multi-Agent Systems against LDLK Specifications

We define the logic LDLK, a formalism for specifying multi-agent systems. LDLK extends LDL with epistemic modalities, including common knowledge, for reasoning about evolution of knowledge states of agents in the system. We show that the problem of verifying multi-agent systems against LDLK specifications is PSPACE-complete. We give an algorithm for practical verification of multi-agent systems specified in LDLK. We show that the model checking algorithm, based on alternating automata and epsilon-NFAs, is fixed parameter tractable, scalable in the size of models analysed, and amenable to symbolic implementation on OBDDs. We introduce MCMAS(LDLK), an extension of the open-source model checker MCMAS implementing the algorithm presented, and discuss the experimental results obtained.