Decidability of Model Checking Multi-Agent Systems with Regular Expressions Against Epistemic HS Specifications

IJCAI 2019 pp. 4746-4752

doi:10.24963/IJCAI.2019/659 /ijcai/2019/michaliszyn2019ijcai-decidability/

Abstract

Epistemic Halpern-Shoham logic (EHS) is an interval temporal logic defined to verify properties of Multi-Agent Systems. In this paper we show that the model checking Multi-Agent Systems with regular expressions against the EHS specifications is decidable. We achieve this by reducing the model checking problem to the satisfiability problem of Monadic Second-Order Logic on trees.

PDF IJCAI Semantic Scholar

Cite

Text

Michaliszyn and Witkowski. "Decidability of Model Checking Multi-Agent Systems with Regular Expressions Against Epistemic HS Specifications." International Joint Conference on Artificial Intelligence, 2019. doi:10.24963/IJCAI.2019/659

Markdown

[Michaliszyn and Witkowski. "Decidability of Model Checking Multi-Agent Systems with Regular Expressions Against Epistemic HS Specifications." International Joint Conference on Artificial Intelligence, 2019.](https://mlanthology.org/ijcai/2019/michaliszyn2019ijcai-decidability/) doi:10.24963/IJCAI.2019/659

BibTeX

@inproceedings{michaliszyn2019ijcai-decidability,
  title     = {{Decidability of Model Checking Multi-Agent Systems with Regular Expressions Against Epistemic HS Specifications}},
  author    = {Michaliszyn, Jakub and Witkowski, Piotr},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {2019},
  pages     = {4746-4752},
  doi       = {10.24963/IJCAI.2019/659},
  url       = {https://mlanthology.org/ijcai/2019/michaliszyn2019ijcai-decidability/}
}