Sciweavers

STACS
2007
Springer

Bounded-Variable Fragments of Hybrid Logics

13 years 10 months ago
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.
Thomas Schwentick, Volker Weber
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where STACS
Authors Thomas Schwentick, Volker Weber
Comments (0)