2 Search Results for "Kernberger, Daniel"

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-dev.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-dev.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}
}
  • Refine by Author
  • 2 Kernberger, Daniel
  • 2 Lange, Martin

  • Refine by Classification
  • 1 Theory of computation → Modal and temporal logics

  • Refine by Keyword
  • 2 hybrid logics
  • 2 mu-calculus
  • 1 bisimulation invariance
  • 1 branching-time
  • 1 expressiveness
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2017
  • 1 2018

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact