2019 IJCAI IJCAI 2019

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

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.

🧭 Keyword Pioneer — interval temporal logic
🐣 Hot Topic Early Bird — multi-agent system
🐝 Cross-Pollinator — Artificial Intelligence, Computer Science, Deep Learning, Healthcare & Medicine, Interdisciplinary, Knowledge & Reasoning, Machine Learning, Mathematics & Optimization, Natural Language Processing, Reinforcement Learning, Robotics