Document Open Access Logo

On the Expressive Power of Hybrid Branching-Time Logics

Authors Daniel Kernberger, Martin Lange

PDF
Thumbnail PDF

File

LIPIcs.TIME.2018.16.pdf
  • Filesize: 485 kB
  • 18 pages

Document Identifiers

Author Details

Daniel Kernberger
  • School of Electrical Engineering and Computer Science, University of Kassel, Germany
Martin Lange
  • School of Electrical Engineering and Computer Science, University of Kassel, Germany

Cite AsGet BibTex

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

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • branching-time
  • mu-calculus
  • hybrid logics
  • expressiveness

Metrics

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

References

  1. C. Areces, P. Blackburn, and M. Marx. The computational complexity of hybrid temporal logics. Logic J. of the IGPL, 8(5):653-679, 2000. Google Scholar
  2. 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
  3. P. Blackburn. Representation, reasoning, and relational structures: A hybrid logic manifesto. Logic J. of the IGPL, 8(3):339-365, 2000. Google Scholar
  4. S. Demri, V. Goranko, and M. Lange. Temporal Logics in Computer Science, volume I - Finite State Systems of Cambridge Tracts in Theor. Comp. Sc. Cambridge Univ. Press, 2016. Google Scholar
  5. H.-D. Ebbinghaus and J. Flum. Finite Model Theory. Perspectives in Math. Logic. Springer, Berlin, 1995. Google Scholar
  6. A. Ehrenfeucht. An application of games to the completeness problem for formalized theories. Fundamenta Mathematicae, 49:129-141, 1961. Google Scholar
  7. E. A. Emerson and E. M. Clarke. Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming, 2(3):241-266, 1982. Google Scholar
  8. E. A. Emerson and J. Y. Halpern. Decision procedures and expressiveness in the temporal logic of branching time. J. of Comp. and Sys. Sc., 30:1-24, 1985. Google Scholar
  9. E. A. Emerson and J. Y. Halpern. "Sometimes" and "not never" revisited: On branching versus linear time temporal logic. J. of the ACM, 33(1):151-178, 1986. Google Scholar
  10. E. A. Emerson and C. S. Jutla. The complexity of tree automata and logics of programs. SIAM J. on Computing, 29(1):132-158, 2000. 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. Kernberger and M. Lange. The fully hybrid mu-calculus. In Proc. 24th Int. Symp. on Temporal Representation and Reasoning, TIME'17, volume 90 of LIPIcs, pages 17:1-17:16. Dagstuhl-Leibniz-Zentrum, 2017. URL: http://www.dagstuhl.de/dagpub/978-3-95977-052-1.
  14. A. Pnueli. The temporal logic of programs. In Proc. 18th Symp. on Foundations of Computer Science, FOCS'77, pages 46-57, Providence, RI, USA, 1977. IEEE. Google Scholar
  15. 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
  16. M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification (preliminary report). In Proc. 1st Symp. on Logic in Computer Science, LICS'86, pages 332-344. IEEE, Washington, DC, 1986. 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 Imprint Privacy Contact