Model Checking Epistemic Halpern-Shoham Logic Extended with Regular Expressions

TL;DR

This paper extends the Epistemic Halpern-Shoham logic by incorporating regular expressions into its semantics, maintaining known complexity results and introducing a new logic EHSre with comparable expressive power.

Contribution

It generalizes EHS semantics using regular expressions and introduces EHSre, a new logic with equivalent expressive power on Kripke structures.

Findings

Model checking complexity remains unchanged for the generalized logic.

EHSre has expressive power equivalent to EHS with regular expressions.

The semantics extension preserves positive results of EHS.

Abstract

The Epistemic Halpern-Shoham logic (EHS) is a temporal-epistemic logic that combines the interval operators of the Halpern-Shoham logic with epistemic modalities. The semantics of EHS is based on interpreted systems whose labelling function is defined on the endpoints of intervals. We show that this definition can be generalised by allowing the labelling function to be based on the whole interval by means of regular expressions. We prove that all the positive results known for EHS, notably the attractive complexity of its model checking problem for some of its fragments, still hold for its generalisation. We also propose the new logic EHSre which operates on standard Kripke structures and has expressive power equivalent to that of EHS with regular expressions. We compare the expressive power of EHSre with standard temporal logics.