Bounded-variable fragments of hybrid logics

Hybrid logics extend modal logics by first-order concepts, in particular they allow a limited use of variables. Unfortunately, in general, satisfiability for hybrid formulas is undecidable and model checking is PSPACE-hard. It is shown here that on the linear frame (omega, <), the restrict ion to one name, although expressively complete, has EXPSPACE-complete satisfiability and polynomial time model-checking. For the upper bound, a result of independent interest is found: Non-emptiness for alternating two-way Buchi automata with one pebble is EXPSPACE-complete.