Document Open Access Logo

The Fully Hybrid mu-Calculus

Authors Daniel Kernberger, Martin Lange

PDF
Thumbnail PDF

File

LIPIcs.TIME.2017.17.pdf
  • Filesize: 0.51 MB
  • 16 pages

Document Identifiers

Author Details

Daniel Kernberger
Martin Lange

Cite As Get BibTex

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) https://doi.org/10.4230/LIPIcs.TIME.2017.17

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.

Subject Classification

Keywords
  • mu-calculus
  • hybrid logics
  • model checking
  • bisimulation invariance

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. R. Alur and T. A. Henzinger. A really temporal logic. J. of the ACM, 41(1):181-204, 1994. Google Scholar
  2. H. R. Andersen. A polyadic modal μ-calculus. Technical Report ID-TR: 1994-195, Dept. of Computer Science, Technical University of Denmark, Copenhagen, 1994. Google Scholar
  3. C. Areces, P. Blackburn, and M. Marx. Hybrid logics: Characterization, interpolation and complexity. J. of Symb. Log., 66:2001, 1999. Google Scholar
  4. C. Areces and B. ten Cate. Hybrid logics. In P. Blackburn, F. Wolter, and J. van Benthem, editors, Handbook of Modal Logics, pages 821-868. Elsevier, 2006. Google Scholar
  5. J. . Correspondence theory. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, Volume II: Extensions of Classical Logic, pages 167-247. D. Reidel, 1984. Google Scholar
  6. B. S. Chlebus. Domino-tiling games. J. of Comp. and Sys. Sc., 32:374-392, 1986. Google Scholar
  7. M. Dam. CTL^* and ECTL^* as fragments of the modal μ-calculus. TCS, 126(1):77-96, 1994. Google Scholar
  8. E. A. Emerson, C. S. Jutla, and A. P. Sistla. On model-checking for fragments of μ-calculus. In Proc. 5th Conf. on Computer Aided Verification, CAV'93, volume 697 of LNCS, pages 385-396. Springer, 1993. Google Scholar
  9. M. Franceschet and M. . Model checking hybrid logics (with an application to semistructured data). J. of Applied Logic, 4(3):279-304, 2006. Google Scholar
  10. M. Jurdziński. Deciding the winner in parity games is in UP∩co-UP. Inf. Process. Lett., 68(3):119-124, 1998. Google Scholar
  11. A. Kara, V. Weber, M. Lange, and T. Schwentick. On the hybrid extension of CTL and CTL^+. In Proc. 34th Int. Symp. on Mathematical Foundations of Computer Science, MFCS'09, volume 5734 of LNCS, pages 427-438. Springer, 2009. Google Scholar
  12. D. Kernberger and M. Lange. Model checking for the full hybrid computation tree logic. In Proc. 23rd Int. Symp. on Temporal Representation and Reasoning, TIME'16, pages 31-40. IEEE Computer Society, 2016. Google Scholar
  13. D. Kozen. Results on the propositional μ-calculus. TCS, 27:333-354, 1983. Google Scholar
  14. M. Lange and E. Lozes. Model checking the higher-dimensional modal μ-calculus. In Proc. 8th Workshop on Fixpoints in Computer Science, FICS'12, volume 77 of Electr. Proc. in Theor. Comp. Sc., pages 39-46, 2012. Google Scholar
  15. M. Otto. Bisimulation-invariant PTIME and higher-dimensional μ-calculus. Theor. Comput. Sci., 224(1-2):237-265, 1999. Google Scholar
  16. U. Sattler and M. Y. Vardi. The hybrid μ-calculus. In Proc. 1st Int. Joint Conf. on Automated Reasoning, IJCAR'01, volume 2083 of LNCS, pages 76-91. Springer, 2001. Google Scholar
  17. C. Stirling. Local model checking games. In Proc. 6th Conf. on Concurrency Theory, CONCUR'95, volume 962 of LNCS, pages 1-11. Springer, 1995. Google Scholar
  18. C. Stirling. Bisimulation, modal logic and model checking games. Logic J. of the IGPL, 7(1):103-124, 1999. Google Scholar
  19. B. ten Cate. Model theory for extended modal languages. PhD thesis, Institute for Logic, Language and Computation, University of Amsterdam, Amsterdam, The Netherlands, 2005. Google Scholar
  20. J. Vöge and M. Jurdziński. A discrete strategy improvement algorithm for solving parity games. In Proc. 12th Int. Conf. on Computer Aided Verification, CAV'00, volume 1855 of LNCS, pages 202-215. Springer, 2000. Google Scholar
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 About DROPS Imprint Privacy Contact