Bounded-Variable Fragments Of Hybrid Logics
STACS'07: Proceedings of the 24th annual conference on Theoretical aspects of computer science(2007)
摘要
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.
更多查看译文
关键词
Model Check, Temporal Logic, Kripke Structure, Hybrid Logic, Model Check Problem
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络