DROPS

Document

DOI: 10.4230/LIPIcs.TIME.2018.16

On the Expressive Power of Hybrid Branching-Time Logics

Authors: Daniel Kernberger and Martin Lange

Published in: LIPIcs, Volume 120, 25th International Symposium on Temporal Representation and Reasoning (TIME 2018)

Abstract

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.

Cite as

Daniel Kernberger and Martin Lange. On the Expressive Power of Hybrid Branching-Time Logics. In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{kernberger_et_al:LIPIcs.TIME.2018.16,
  author =	{Kernberger, Daniel and Lange, Martin},
  title =	{{On the Expressive Power of Hybrid Branching-Time Logics}},
  booktitle =	{25th International Symposium on Temporal Representation and Reasoning (TIME 2018)},
  pages =	{16:1--16:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-089-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{120},
  editor =	{Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.16},
  URN =		{urn:nbn:de:0030-drops-97816},
  doi =		{10.4230/LIPIcs.TIME.2018.16},
  annote =	{Keywords: branching-time, mu-calculus, hybrid logics, expressiveness}
}

Document

DOI: 10.4230/LIPIcs.TIME.2017.17

The Fully Hybrid mu-Calculus

Authors: Daniel Kernberger and Martin Lange

Published in: LIPIcs, Volume 90, 24th International Symposium on Temporal Representation and Reasoning (TIME 2017)

Abstract

We consider the hybridisation of the mu-calculus through the addition of nominals, binder and jump. Especially the use of the binder differentiates our approach from earlier hybridisations of the mu-calculus and also results in a more involved formal semantics. We then investigate the model checking problem and obtain ExpTime-completeness for the full logic and the same complexity as the modal mu-calculus for a fixed number of variables. We also show that this logic is invariant under hybrid bisimulation and use this result to show that - contrary to the non-hybrid case - the hybrid extension of the full branching time logic CTL* is not a fragment of the fully hybrid mu-calculus.

Cite as

Daniel Kernberger and Martin Lange. The Fully Hybrid mu-Calculus. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 17:1-17:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{kernberger_et_al:LIPIcs.TIME.2017.17,
  author =	{Kernberger, Daniel and Lange, Martin},
  title =	{{The Fully Hybrid mu-Calculus}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  pages =	{17:1--17:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-052-1},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{90},
  editor =	{Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.17},
  URN =		{urn:nbn:de:0030-drops-79244},
  doi =		{10.4230/LIPIcs.TIME.2017.17},
  annote =	{Keywords: mu-calculus, hybrid logics, model checking, bisimulation invariance}
}

Search Results

Documents authored by Kernberger, Daniel

On the Expressive Power of Hybrid Branching-Time Logics

Abstract

Cite as

The Fully Hybrid mu-Calculus

Abstract

Cite as

Thanks for your feedback!

Could not send message