Model Checking Multi-Agent Systems Against LDLK Specifications
Abstract
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.
Cite
Text
Kong and Lomuscio. "Model Checking Multi-Agent Systems Against LDLK Specifications." International Joint Conference on Artificial Intelligence, 2017. doi:10.24963/IJCAI.2017/158Markdown
[Kong and Lomuscio. "Model Checking Multi-Agent Systems Against LDLK Specifications." International Joint Conference on Artificial Intelligence, 2017.](https://mlanthology.org/ijcai/2017/kong2017ijcai-model/) doi:10.24963/IJCAI.2017/158BibTeX
@inproceedings{kong2017ijcai-model,
title = {{Model Checking Multi-Agent Systems Against LDLK Specifications}},
author = {Kong, Jeremy and Lomuscio, Alessio},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2017},
pages = {1138-1144},
doi = {10.24963/IJCAI.2017/158},
url = {https://mlanthology.org/ijcai/2017/kong2017ijcai-model/}
}