A BISIMULATION CHARACTERIZATION THEOREM FOR HYBRID LOGIC WITH THE CURRENT-STATE BINDER

We prove that every first-order formula that is invariant under quasi-injective bisim-ulations is equivalent to a formula of the hybrid logic H{jj. Our proof uses a variation of the usual unravelling technique. We also briefly survey related results, and show in a standard way that it is undecidable whether a first-order formula is invariant under quasi-injective bisimulations.