文章基本信息

标题：On the Expressive Power of Hybrid Branching-Time Logics
本地全文：下载
作者：Daniel Kernberger ; Martin Lange
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2018
卷号：120
页码：1-18
DOI：10.4230/LIPIcs.TIME.2018.16
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：Hybrid branching-time logics are a powerful extension of branching-time logics like CTL, CTL^* or even the modal mu-calculus through the addition of binders, jumps and variable tests. Their expressiveness is not restricted by bisimulation-invariance anymore. Hence, they do not retain the tree model property, and the finite model property is equally lost. Their satisfiability problems are typically undecidable, their model checking problems (on finite models) are decidable with complexities ranging from polynomial to non-elementary time. In this paper we study the expressive power of such hybrid branching-time logics beyond some earlier results about their invariance under hybrid bisimulations. In particular, we aim to extend the hierarchy of non-hybrid branching-time logics CTL, CTL^+, CTL^* and the modal mu-calculus to their hybrid extensions. We show that most separation results can be transferred to the hybrid world, even though the required techniques become a bit more involved. We also present some collapse results for restricted classes of models that are especially worth investigating, namely linear, tree-shaped and finite models.
关键词：branching-time; mu-calculus; hybrid logics; expressiveness