Model Checking Temporal Epistemic Logic Under Bounded Recall
Abstract
We study the problem of verifying multi-agent systems under the assumption of bounded recall. We introduce the logic CTLKBR, a bounded-recall variant of the temporal-epistemic logic CTLK. We define and study the model checking problem against CTLK specifications under incomplete information and bounded recall and present complexity upper bounds. We present an extension of the BDD-based model checker MCMAS implementing model checking under bounded recall semantics and discuss the experimental results obtained.
Cite
Text
Belardinelli et al. "Model Checking Temporal Epistemic Logic Under Bounded Recall." AAAI Conference on Artificial Intelligence, 2020. doi:10.1609/AAAI.V34I05.6193Markdown
[Belardinelli et al. "Model Checking Temporal Epistemic Logic Under Bounded Recall." AAAI Conference on Artificial Intelligence, 2020.](https://mlanthology.org/aaai/2020/belardinelli2020aaai-model/) doi:10.1609/AAAI.V34I05.6193BibTeX
@inproceedings{belardinelli2020aaai-model,
title = {{Model Checking Temporal Epistemic Logic Under Bounded Recall}},
author = {Belardinelli, Francesco and Lomuscio, Alessio and Yu, Emily},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2020},
pages = {7071-7078},
doi = {10.1609/AAAI.V34I05.6193},
url = {https://mlanthology.org/aaai/2020/belardinelli2020aaai-model/}
}