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},
title = {Model Checking Epistemic Halpern-Shoham Logic Extended with Regular Expressions},
url = {},
year = {2015}

RIS format (EndNote, RefMan)

AB - The Epistemic Halpern-Shoham logic (EHS) is a temporal-epistemic logic thatcombines the interval operators of the Halpern-Shoham logic with epistemicmodalities. The semantics of EHS is based on interpreted systems whoselabelling function is defined on the endpoints of intervals. We show that thisdefinition can be generalised by allowing the labelling function to be based onthe whole interval by means of regular expressions. We prove that all thepositive results known for EHS, notably the attractive complexity of its modelchecking problem for some of its fragments, still hold for its generalisation.We also propose the new logic EHSre which operates on standard Kripkestructures and has expressive power equivalent to that of EHS with regularexpressions. We compare the expressive power of EHSre with standard temporallogics.
AU - Lomuscio,A
AU - Michaliszyn,J
PY - 2015///
TI - Model Checking Epistemic Halpern-Shoham Logic Extended with Regular Expressions
UR -
ER -