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 (ω, <), the restriction to one name, although expressively complete, has EXPSPACEcomplete satisfiability and polynomial time model-checking. For the upper bound, a result of independent interest is found: Nonemptiness for alternating two-way B¨uchi automata with one pebble is EXPSPACE-complete.

• Type: Conference
• Year: 2007
• Where: STACS
• Authors: Thomas Schwentick, Volker Weber
• Keywords: Hybrid Formulas, Hybrid Logics, Modal Logics, STACS 2007, Theoretical Computer Science