Imperial College London


Faculty of EngineeringDepartment of Computing

Professor of Logic for Multiagent Systems



+44 (0)20 7594 8414a.lomuscio Website




504Huxley BuildingSouth Kensington Campus






BibTex format

author = {Lomuscio, A and Michaliszyn, J},
pages = {298--307},
title = {Model checking multi-agent systems against epistemic HS specifications with regular expressions},
url = {},
year = {2016}

RIS format (EndNote, RefMan)

AB - Copyright © 2016, Association for the Advancement of Artificial Intelligence ( All rights reserved. We introduce EHS+, a novel temporal-epistemic logic defined on temporal intervals characterised by regular expressions. We investigate the complexity of verifying multi-agent systems against EHS+ specifications for a number of fragments of EHS+ with results ranging from PSPACE-completeness to non-elementary time. The findings show that, at least for the fragments under analysis, the increase in expressiveness obtained by using regular expressions rather than end-points as standard, can be achieved without increasing the complexity of the problem. We show that the expressiveness of regular expressions can also be adopted at the level of specifications without severe computational cost. To do so we introduce a further temporal-epistemic logic, called EHSRE, in which regular expressions are used within propositions, and give a polynomial time reduction of the model checking problem from EHSRE to EHS+.
AU - Lomuscio,A
AU - Michaliszyn,J
EP - 307
PY - 2016///
SP - 298
TI - Model checking multi-agent systems against epistemic HS specifications with regular expressions
UR -
ER -