Abstract
We provide several effective equivalent characterizations of EF (the modal logic of the descendant relation) on arbitrary trees. More specifically, we prove that, for EF-bisimulation invariant properties of trees, being definable by an EF formula, being a Borel set, and being definable in weak monadic second order logic, all coincide. The proof builds upon a known algebraic characterization of EF for the case of finitely branching trees due to Bojańczyk and Idziaszek. We furthermore obtain characterizations of modal logic on transitive Kripke structures as a fragment of weak monadic second order logic and of the μ-calculus.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Benedikt, M., Segoufin, L.: Regular Tree Languages Definable in FO and in FO mod . ACM Trans. on Computational Logic 11(1) (2009)
van Benthem, J.: Modal Correspondence Theory. PhD thesis, Mathematisch Instituut & Instituut voor Grondslagenonderzoek, University of Amsterdam (1976)
Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge Univ. Press, Cambridge (2001)
Bojańczyk, M.: Two-Way Unary Temporal Logic over Trees. In: LICS 2007, pp. 121–130 (2007)
Bojańczyk, M., Idziaszek, T.: Algebra for Infinite Forests with an Application to the Temporal Logic EF. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 131–145. Springer, Heidelberg (2009)
Bojańczyk, M., Segoufin, L., Straubing, H.: Piecewise Testable Tree Languages. In: LICS 2008, pp. 442–451 (2008)
Bojańczyk, M., Segoufin, L.: Tree languages defined in first-order logic with one quantifier alternation. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol. 5126, pp. 233–245. Springer, Heidelberg (2008)
Bojańczyk, M., Walukiewicz, I.: Characterizing EF and EX Tree Logics. Theoretical Computer Science 358(2-3), 255–272 (2006)
Bojańczyk, M., Walukiewicz, I.: Forest Algebras. In: Automata and Logic: History and Perspectives, pp. 107–132. Amsterdam University Press, Amsterdam (2007)
Bradfield, J., Stirling, C.: Modal Logic and Mu-Calculi. In: Bergstra, J., et al. (eds.) Handbook of Process Algebra, pp. 293–332. Elsevier, North-Holland (2001)
Dawar, A., Otto, M.: Modal Characterisation Theorems over Special Classes of Frames. Ann. Pure Appl. Logic 161(1), 1–42 (2009)
Janin, D., Walukiewicz, I.: On the Expressive Completeness of the Propositional μ-Calculus with Respect to Monadic Second Order Logic. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 263–277. Springer, Heidelberg (1996)
Murlak, F.: Weak Index vs Borel Rank. In: STACS 2008, pp. 573–584 (2008)
Otto, M.: Eliminating recursion in the μ-calculus. In: Meinel, C., Tison, S. (eds.) STACS 1999. LNCS, vol. 1563, pp. 531–540. Springer, Heidelberg (1999)
Place, T.: Characterization of logics over ranked tree languages. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 401–415. Springer, Heidelberg (2008)
Walukiewicz, I.: Monadic Second-Order Logic on Tree-Like Structures. Theoretical Computer Science 275(1-2), 311–346 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag GmbH Berlin Heidelberg
About this paper
Cite this paper
ten Cate, B., Facchini, A. (2011). Characterizing EF over Infinite Trees and Modal Logic on Transitive Graphs. In: Murlak, F., Sankowski, P. (eds) Mathematical Foundations of Computer Science 2011. MFCS 2011. Lecture Notes in Computer Science, vol 6907. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22993-0_28
Download citation
DOI: https://doi.org/10.1007/978-3-642-22993-0_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22992-3
Online ISBN: 978-3-642-22993-0
eBook Packages: Computer ScienceComputer Science (R0)