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
-hard. It is shown here that on the linear frame (
, < ), the restriction to one name, although expressively complete, has
-complete satisfiability and polynomial time model-checking.
For the upper bound, a result of independent interest is found: Non-emptiness for alternating two-way Büchi automata with one pebble is