Skip to main content
SpringerLink
Log in

Monadic Second-Order Logic and Automata

  • Chapter
Elements of Finite Model Theory

Part of the book series: Texts in Theoretical Computer Science ((TTCS))

  • 1091 Accesses

Abstract

We now move to extensions of first-order logic. In this chapter we introduce second-order logic, and consider its often used fragment, monadic second-order logic,or MSO, in which one can quantify over subsets of the universe. We study the expressive power of this logic over graphs, proving that its existential fragment expresses some NP-complete problems, but at the same time cannot express graph connectivity. Then we restrict our attention to strings and trees, and show that, over them, MSO captures regular string and tree languages. We explore the connection with automata to prove further definability and complexity results.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 79.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 99.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 99.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. H.-D. Ebbinghaus and J. Flum. Finite Model Theory. Springer-Verlag, 1995.

    Google Scholar 

  2. R. Fagin. Monadic generalized spectra. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 21 (1975), 89–96.

    Article  MathSciNet  MATH  Google Scholar 

  3. R. Fagin, L. Stockmeyer, and M.Y. Vardi. On monadic NP vs monadic co-NP. Information and Computation, 120 (1994), 78–92.

    Article  MathSciNet  Google Scholar 

  4. M. Ajtai and R. Fagin. Reachability is harder for directed than for undirected graphs. Journal of Symbolic Logic, 55 (1990), 113–150.

    Article  MathSciNet  MATH  Google Scholar 

  5. R. Fagin. Easier ways to win logical games. In [134], pages 1–32.

    Google Scholar 

  6. M. Ajtai, R. Fagin, and L. Stockmeyer. The closure of monadic NP. Journal of Computer and System Sciences, 60 (2000), 660–716.

    Article  MathSciNet  MATH  Google Scholar 

  7. D. Janin and J. Marcinkowski. A toolkit for first order extensions of monadic games. Proc. of Symp. on Theoretical Aspects of Computer Science, Springer-Verlag LNCS vol. 2010, Springer Verlag, 2001, 351–364.

    Google Scholar 

  8. T. Schwentick. Descriptive complexity, lower bounds and linear time. In Proc. of Computer Science Logic, Springer-Verlag LNCS 1584, 1998, pages 9–28.

    Google Scholar 

  9. J.R. Büchi. Weak second-order arithmetic and finite automata. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 6 (1960), 66–92.

    Article  MATH  Google Scholar 

  10. R.E. Ladner. Application of model theoretic games to discrete linear orders and finite automata. Information and Control, 33 (1977), 281–303.

    Article  MathSciNet  MATH  Google Scholar 

  11. F. Neven and T. Schwentick. Query automata on finite trees. Theoretical Computer Science, 275 (2002), 633–674.

    Article  MathSciNet  MATH  Google Scholar 

  12. G. Turän. On the definability of properties of finite graphs. Discrete Mathematics, 49 (1984), 291–302.

    Article  MathSciNet  Google Scholar 

  13. M. de Rougemont. Second-order and inductive definability on finite structures. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 33 (1987), 47–63.

    Article  MATH  Google Scholar 

  14. J. Makowsky. Model theory and computer science: an appetizer. In Handbook of Logic in Computer Science, Vol. 1, Oxford University Press, 1992.

    Google Scholar 

  15. R. McNaughton and S. Papert. Counter-Free Automata. MIT Press, 1971.

    Google Scholar 

  16. W. Thomas. Languages, automata, and logic. In Handbook of Formal Languages, Vol. 3, Springer-Verlag, 1997, pages 389–455.

    Google Scholar 

  17. H. Straubing. Finite Automata, Formal Logic, and Circuit Complexity. Birkhäuser, 1994.

    Google Scholar 

  18. S. Feferman and R. Vaught. The first order properties of products of algebraic systems. Fundamenta Mathematicae, 47 (1959), 57–103.

    MathSciNet  MATH  Google Scholar 

  19. J. Makowsky. Algorithmic aspects of the Feferman-Vaught Theorem. Annals of Pure and Applied Logic, 126 (2004), 159–213.

    Article  MathSciNet  MATH  Google Scholar 

  20. H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree Automata: Techniques and Applications. Available at www.grappa.univ-1111e3.fr/tata. October 2002.

    Google Scholar 

  21. F. Gécseg and M. Steinby. Tree languages. In Handbook of Formal Languages, Vol. 3. Springer-Verlag, 1997, pages 1–68.

    Google Scholar 

  22. J. Thatcher and J. Wright. Generalized finite automata theory with an application to a decision problem of second-order logic. Mathematical Systems Theory, 2 (1968), 57–81.

    Article  MathSciNet  Google Scholar 

  23. F. Neven. Automata theory for XML researchers. SIGMOD Record, 31 (2002), 39–46.

    Article  Google Scholar 

  24. L. Stockmeyer. The polynomial-time hierarchy. Theoretical Computer Science, 3 (1977), 1–22.

    Article  MathSciNet  MATH  Google Scholar 

  25. D.-Z. Du, K.-I. Ko. Theory of Computational Complexity. Wiley-Interscience, 2000.

    Google Scholar 

  26. B. Courcelle. Graph rewriting: an algebraic and logic approach. In Handbook of Theoretical Computer Science, Vol. B, North-Holland, 1990, pages 193–242.

    Google Scholar 

  27. H. Bodlaender. A linear-time algorithm for finding tree-decompositions of small treewidth. SIAM Journal on Computing, 25 (1996), 1305–1317.

    Article  MathSciNet  MATH  Google Scholar 

  28. L. Stockmeyer and A. Meyer. Cosmological lower bound on the circuit complexity of a small problem in logic. Journal of the ACM, 49 (2002), 753 784.

    MathSciNet  Google Scholar 

  29. B. Courcelle. On the expression of graph properties in some fragments of monadic second-order logic. In [134], pages 33–62.

    Google Scholar 

  30. B. Courcelle. The monadic second-order logic on graphs VI: on several representations of graphs by relational structures. Discrete Applied Mathematics, 54 (1994), 117–149.

    Article  MathSciNet  MATH  Google Scholar 

  31. T. Schwentick. On winning Ehrenfeucht games and monadic NP. Annals of Pure and Applied Logic, 79 (1996), 61–92.

    Article  MathSciNet  MATH  Google Scholar 

  32. S. Cosmadakis. Logical reducibility and monadic NP. In Proc. IEEE Symp. on Foundations of Computer Science, 1993, pages 52–61.

    Google Scholar 

  33. M. Otto. A note on the number of monadic quantifiers in monadic 1’1. Information Processing Letters, 53 (1995), 337–339.

    Article  MathSciNet  MATH  Google Scholar 

  34. O. Matz, N. Schweikardt, and W. Thomas. The monadic quantifier alternation hierarchy over grids and graphs. Information and Computation, 179 (2002), 356–383.

    Article  MathSciNet  MATH  Google Scholar 

  35. W. Thomas. Classifying regular events in symbolic logic. Journal of Computer and System Sciences, 25 (1982), 360–376.

    Article  MathSciNet  MATH  Google Scholar 

  36. W. Thomas. Logical aspects in the study of tree languages. In Proc. 9th Int. Colloq. on Trees in Algebra and Programming (CAAP’84), Cambridge University Press, 1984, pages 31 50.

    Google Scholar 

  37. A. Blumensath and E. Grädel. Automatic structures. In IEEE Symp. on Logic in Computer Science, 2000, pages 51–62.

    Google Scholar 

  38. V. Bruyère, G. Hansel, C. Michaux, and R. Villemaire. Logic and p-recognizable sets of integers. Bulletin of the Belgian Mathematical Society, 1 (1994), 191–238.

    MATH  Google Scholar 

  39. M. Benedikt, L. Libkin, T. Schwentick, and L. Segoufin. Definable relations and first-order query languages over strings. Journal of the ACM, 50 (2003), 694–751.

    Article  MathSciNet  Google Scholar 

  40. M. Benedikt and L. Libkin. Tree extension algebras: logics, automata, and query languages. In IEEE Symp. on Logic in Computer Science, 2002, pages 203–212.

    Google Scholar 

  41. M. Frick and M. Grohe. The complexity of first-order and monadic second-order logic revisited. In IEEE Symp. on Logic in Computer Science, 2002, pages 215–224.

    Google Scholar 

  42. E. Grandjean and F. Olive. Monadic logical definability of nondeterministic linear time. Computational Complexity, 7 (1998), 54–97.

    Article  MathSciNet  MATH  Google Scholar 

  43. J. Lynch. Complexity classes and theories of finite models. Mathematical Systems Theory, 15 (1982), 127–144.

    Article  MathSciNet  MATH  Google Scholar 

  44. B. Courcelle and J. Makowsky. Fusion in relational structures and the verification of monadic second-order properties. Mathematical Structures in Computer Science, 12 (2002), 203–235.

    Article  MathSciNet  MATH  Google Scholar 

  45. D. Seese. The structure of models of decidable monadic theories of graphs. Annals of Pure and Applied Logic, 53 (1991), 169–195.

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Toronto, M5S 3H5, Toronto, ON, Canada

    Prof. Leonid Libkin

Authors
  1. Prof. Leonid Libkin
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Libkin, L. (2004). Monadic Second-Order Logic and Automata. In: Elements of Finite Model Theory. Texts in Theoretical Computer Science. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-07003-1_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-07003-1_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-05948-3

  • Online ISBN: 978-3-662-07003-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation