On the Expressive Power of Hybrid Branching-Time Logics
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.
branching-time
mu-calculus
hybrid logics
expressiveness
Theory of computation~Modal and temporal logics
16:1-16:18
Regular Paper
Daniel
Kernberger
Daniel Kernberger
School of Electrical Engineering and Computer Science, University of Kassel, Germany
Martin
Lange
Martin Lange
School of Electrical Engineering and Computer Science, University of Kassel, Germany
10.4230/LIPIcs.TIME.2018.16
C. Areces, P. Blackburn, and M. Marx. The computational complexity of hybrid temporal logics. Logic J. of the IGPL, 8(5):653-679, 2000.
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.
P. Blackburn. Representation, reasoning, and relational structures: A hybrid logic manifesto. Logic J. of the IGPL, 8(3):339-365, 2000.
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.
H.-D. Ebbinghaus and J. Flum. Finite Model Theory. Perspectives in Math. Logic. Springer, Berlin, 1995.
A. Ehrenfeucht. An application of games to the completeness problem for formalized theories. Fundamenta Mathematicae, 49:129-141, 1961.
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.
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.
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.
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.
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.
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.
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.
http://www.dagstuhl.de/dagpub/978-3-95977-052-1
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.
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.
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.
Daniel Kernberger and Martin Lange
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode