Paper detail

A modular bisimulation characterisation for fragments of hybrid logic

There are known characterisations of several fragments of hybrid logic by means of invariance under bisimulations of some kind. The fragments include $\{\store, \jump\}$ with or without nominals (Areces, Blackburn, Marx), $\jump$ with or without nominals (ten Cate), and $\store$ without nominals (Hodkinson, Tahiri). Some pairs of these characterisations, however, are incompatible with one another. For other fragments of hybrid logic no such characterisations were known so far. We prove a generic bisimulation characterisation theorem for all standard fragments of hybrid logic, in particular for the case with $\store$ and nominals, left open by Hodkinson and Tahiri. Our characterisation is built on a common base and for each feature extension adds a specific condition, so it is modular in an engineering sense.