659@2019@IJCAI

#1 Decidability of Model Checking Multi-Agent Systems with Regular Expressions against Epistemic HS Specifications [PDF] [Copy] [Kimi] [REL]

Authors: Jakub Michaliszyn ; Piotr Witkowski

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.