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, AR and Michaliszyn, J},
pages = {298--307},
publisher = {Association for the Advancement of Artificial Intelligence},
title = {Model Checking Multi-Agent Systems against Epistemic HS Specifications with Regular Expressions},
url = {},
year = {2016}

RIS format (EndNote, RefMan)

AB - We introduce EHS+, a novel temporal-epistemic logic definedon temporal intervals characterised by regular expressions.We investigate the complexity of verifying multi-agent systemsagainst EHS+specifications for a number of fragmentsof EHS+ with results ranging from PSPACE-completeness tonon-elementary time. The findings show that, at least for thefragments under analysis, the increase in expressiveness obtainedby using regular expressions rather than end-points asstandard, can be achieved without increasing the complexityof the problem. We show that the expressiveness of regularexpressions can also be adopted at the level of specificationswithout severe computational cost. To do so we introducea further temporal-epistemic logic, called EHSRE, in whichregular expressions are used within propositions, and give apolynomial time reduction of the model checking problemfrom EHSRE to EHS+.
AU - Lomuscio,AR
AU - Michaliszyn,J
EP - 307
PB - Association for the Advancement of Artificial Intelligence
PY - 2016///
SP - 298
TI - Model Checking Multi-Agent Systems against Epistemic HS Specifications with Regular Expressions
UR -
UR -
ER -