Monadic second order logic on tree-like structures

  • Igor Walukiewicz
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1046)


An operation M+ constructing from a given structure M a tree-like structure which domain consists of the sequences of elements of M is considered. A notion of automata running on such tree-like structures is defined. This notion is parametrised by a set of basic formulas. It is shown that if basic formulas satisfy some conditions then the class of languages recognised by automata is closed under disjunction, complementation and projection. For one choice of basic formulas we obtain a characterisation of MSOL over tree-like structures. This characterisation allows us to show that MSOL theory of tree-like structures is effectively reducible to that of the original structures. For a different choice of basic formulas we obtain a characterisation of MSOL on trees of arbitrary degree and the proof that it is equivalent to the first order logic extended with the unary least fixpoint operator.


Binary Tree Order Variable Order Logic Basic Formula Relational Symbol 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    J. Büchi. State strategies for games in Fσδ∩Gσδ. Journal of Symbolic Logic, 48:1171–1198, 1983.Google Scholar
  2. [2]
    B. Courcelle. The monadic second-order logic on graphs IX: machines and behaviours. Theoretical Computer Science, 149, 1995.Google Scholar
  3. [3]
    B. Courcelle and I. Walukiewicz. Monadic second-order logic, graphs and unfoldings of transition systems. University of Aarhus BRICS report RS-95-44. Presented at CSL'95.Google Scholar
  4. [4]
    E. Emerson and C. Jutla. Tree automata, mu-calculus and determinacy. In Proc. FOCS 91, 1991.Google Scholar
  5. [5]
    Y. Gurevich and L. Harrington. Trees, automata and games. In 14th Symp. on Theory of Computations, ACM, pages 60–65, 1982.Google Scholar
  6. [6]
    D. Janin and I. Walukiewicz. Automata for the μ-calculus and related results. In MFCS'95, volume 969 of LNCS, pages 552–562, 1995.Google Scholar
  7. [7]
    A. W. Mostowski. Regular expressions for infinite trees and a standard form of automata. In A. Skowron, editor, Fifth Symposium on Computation Theory, volume 208 of LNCS, pages 157–168, 1984.Google Scholar
  8. [8]
    A. W. Mostowski. Games with forbidden positions. Technical Report 78, University of Gdansk, 1991.Google Scholar
  9. [9]
    D. Niwiński. Fixed points vs. infinite generation. In Proc. 3rd. IEEE LICS, pages 402–409, 1988.Google Scholar
  10. [10]
    M. Rabin. Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc., 141:1–35, 1969.Google Scholar
  11. [11]
    A. Semenov. Decidability of monadic theories. In MFCS'84, volume 176 of LNCS, pages 162–175. Springer-Verlag, 1984.Google Scholar
  12. [12]
    S. Shelah. The monadic second order theory of order. Annals of Mathematics, 102:379–419, 1975.Google Scholar
  13. [13]
    W. Thomas. Automata on infinite objects. In J. Leeuven, editor, Handbook of Theoretical Computer Science Vol. B, pages 995–1072. Elesvier, 1990.Google Scholar
  14. [14]
    W. Thomas. On logics, tilings, and automata. In ICALP '91, volume 510 of LNCS, pages 441–454, 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

  • Igor Walukiewicz
    • 1
  1. 1.Basic Research in Computer Science, Centre of the Danish National Research Foundation Department of Computer ScienceUniversity of AarhusAarhus CDenmark

Personalised recommendations