Decidability of Model Checking Multi-Agent Systems with Regular Expressions against Epistemic HS Specifications
Decidability of Model Checking Multi-Agent Systems with Regular Expressions against Epistemic HS Specifications
Jakub Michaliszyn, Piotr Witkowski
Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence
Main track. Pages 4746-4752.
https://doi.org/10.24963/ijcai.2019/659
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.
Keywords:
Multidisciplinary Topics and Applications: Validation and Verification
Agent-based and Multi-agent Systems: Formal Verification, Validation and Synthesis