eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-09-25
17:1
17:16
10.4230/LIPIcs.TIME.2017.17
article
The Fully Hybrid mu-Calculus
Kernberger, Daniel
Lange, Martin
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol090-time2017/LIPIcs.TIME.2017.17/LIPIcs.TIME.2017.17.pdf
mu-calculus
hybrid logics
model checking
bisimulation invariance