Hybrid Logics. Characterization, Interpolation and Complexity
Carlos Areces, Patrick Blackburn, Maarten Marx

Abstract:
Hybrid languages are extended modal languages which can refer to (or even 
quantify over) worlds.  The use of strong hybrid languages dates back to at 
least \cite{prio:past67}, but recent work (for example \cite{blac:hybr98},
\cite{blac:hybr98a}) has focused  on a more constrained system called
$\mathcal{H}(\downarrow,@)$.  The purpose of the present paper is to show 
in detail that $\mathcal{H}(\downarrow,@)$ is a modally natural system.  
We begin by studying its  expressivity, and provide both model theoretic
characterizations (via a restricted notion of Ehrenfeucht-Fra\"{\i}ss\'e 
game, and an enriched notion of bisimulation) and a syntactic characteri-
zation (in terms of bounded formulas).  The key result to emerge is that 
$\mathcal{H}(\downarrow,@)$ corresponds precisely to the first-order 
fragment which is invariant for generated submodels.  We further establish 
that $\mathcal{H}(\downarrow,@)$ has (strong) interpolation, and provide 
failure results in the finite variable fragments.  We also show that weak 
interpolation holds for the sublanguage $\mathcal{H}(@)$, and provide
complexity results for $\mathcal{H}(@)$ and other fragments and variants 
(the full logic being undecidable).