Skip to main content

Finite Model Theory and Descriptive Complexity

  • Chapter
Finite Model Theory and Its Applications

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

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

Access this chapter

eBook
USD 16.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.00
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. S. Abiteboul, R. Hull, and V. Vianu. Foundations of Databases. Addison-Wesley, 1995.

    Google Scholar 

  2. S. Abiteboul and V. Vianu. Datalog extensions for database queries and updates. Journal of Computer and System Sciences, 43:62–124, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  3. H. Andréka, J. van Benthem, and I. Németi. Modal languages and bounded fragments of predicate logic. Journal of Philosophical Logic, 27:217–274, 1998.

    Article  MATH  MathSciNet  Google Scholar 

  4. A. Arnold. The mu-calculus alternation-depth is strict on binary trees. RAIRO Informatique Théorique et Applications, 33:329–339, 1999.

    Article  MATH  Google Scholar 

  5. A. Arnold and D. Niwiński. Rudiments of μ-Calculus. North-Holland, 2001.

    Google Scholar 

  6. C. Ash and J. Knight. Computable Structures and the Hyperarithmetical Hierarchy. Elsevier, 2000.

    Google Scholar 

  7. G. Asser. Das Repräsentantenproblem im PrädikatenkalkĂ¼l der ersten Stufe mit Identität. Zeitschrift fĂ¼r Mathematische Logik und Grundlagen der Mathematik, 1:252–263, 1955.

    Article  MATH  MathSciNet  Google Scholar 

  8. L. Babai, P. Erdös, and S. Selkow. Random graph isomorphism. SIAM Journal of Computing, 9:628–635, 1980.

    Article  MATH  Google Scholar 

  9. J. BalcĂ¡zar, J. DĂ­az, and J. GabarrĂ³. Structural Complexity II. Springer, 1990.

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  11. D. Berwanger and A. Blumensath. The monadic theory of tree-like structures. In E. Grädel, W. Thomas, and T. Wilke, editors, Automata, Logic, and Infinite Games. Springer, 2002.

    Google Scholar 

  12. H. Björklund, S. Sandberg, and S. Vorobyov. Memoryless determinacy of parity and mean payoff games: A simple proof. Theoretical Computer Science, 310:365–378, 2003.

    Article  Google Scholar 

  13. A. Blass and Y. Gurevich. Existential fixed point logic. In E. Börger, editor, Computation Theory and Logic, Lecture Notes in Computer Science, No. 270, pages 20–36. Springer, 1987.

    Google Scholar 

  14. L. Blum, F. Cucker, M. Shub, and S. Smale. Complexity and Real Computation. Springer, 1998.

    Google Scholar 

  15. L. Blum, M. Shub, and S. Smale. On a theory of computation and complexity over the real numbers. Bulletin of AMS, 21:1–46, 1989.

    Article  MATH  MathSciNet  Google Scholar 

  16. A. Blumensath. Automatic structures. Diplomarbeit, RWTH Aachen, 1999.

    Google Scholar 

  17. A. Blumensath. Prefix-recognisable graphs and monadic second-order logic. Technical Report AIB-06-2001, RWTH Aachen, 2001.

    Google Scholar 

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

    Google Scholar 

  19. A. Blumensath and E. Grädel. Finite presentations of infinite structures: Automata and interpretations. Theory of Computing Systems, 37:641–674, 2004.

    Article  MATH  MathSciNet  Google Scholar 

  20. J. Bradfield. The modal μ-calculus alternation hierarchy is strict. Theoretical Computer Science, 195:133–153, 1998.

    Article  MATH  MathSciNet  Google Scholar 

  21. J. Bradfield and C. Stirling. Modal logics and mu-calculi. In J. Bergstra, A. Ponse, and S. Smolka, editors, Handbook of Process Algebra, pages 293–332. Elsevier, 2001.

    Google Scholar 

  22. P. BĂ¼rgisser, M. Clausen, and A. Shokrollahi. Algebraic Complexity Theory. Springer, 1997.

    Google Scholar 

  23. J. Cai, M. FĂ¼rer, and N. Immerman. An optimal lower bound on the number of variables for graph identification. Combinatorica, 12:389–410, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  24. A. Carayol and S. Wöhrle. The caucal hierarchy of infinite graphs in terms of logic and higher-order pushdown automata. In Proceedings of FSTTCS, Lecture Notes in Computer Science, No. 2914, Springer, 2003.

    Google Scholar 

  25. D. Caucal. On infinite transition graphs having a decidable monadic theory. In Automata, Languages and Programming, 23rd International Colloquium, ICALP96, Lecture Notes in Computer Science, No. 1099, pages 194–205. Springer, 1996.

    Google Scholar 

  26. D. Caucal. On infinite terms having a decidable monadic theory. In Proceedings of 27th International Symposium on Mathematical Foundations of Computer Science MFCS 02, Lecture Notes in Computer Science, No. 2420, pages 165–176. Springer, 2002.

    Google Scholar 

  27. B. Courcelle. The monadic second-order logic of graphs II: Infinite graphs of bounded width. Mathematical Systems Theory, 21:187–221, 1989.

    Article  MATH  MathSciNet  Google Scholar 

  28. B. Courcelle. The monadic second-order logic of graphs IX: Machines and their behaviours. Theoretical Computer Science, 151:125–162, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  29. B. Courcelle and I. Walukiewicz. Monadic second-order logic, graph coverings and unfoldings of transition systems. Annals of Pure and Applied Logic, 92:35–62, 1998.

    Article  MATH  MathSciNet  Google Scholar 

  30. F. Cucker and K. Meer. Logic which capture complexity classes over the reals. Journal of Symbolic Logic, 64:363–390, 1999.

    Article  MATH  MathSciNet  Google Scholar 

  31. E. Dahlhaus. Skolem normal forms concerning the least fixed point. In E. Börger, editor, Computation Theory and Logic, Lecture Notes in Computer Science, No. 270, pages 101–106, Springer, 1987.

    Google Scholar 

  32. A. Dawar. Generalized quantifiers and logical reducibilities. Journal of Logic and Computation, 5:213–226, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  33. A. Dawar, E. Grädel, and S. Kreutzer. Inflationary fixed points in modal logic. ACM Transactions on Computational Logic, 5:282–315, 2004.

    Article  MathSciNet  Google Scholar 

  34. A. Dawar, E. Grädel, and S. Kreutzer. Backtracking games and inflationary fixed points. Theoretical Computer Science, 350:174–187, 2006.

    Article  MATH  MathSciNet  Google Scholar 

  35. A. Dawar and L. Hella. The expressive power of finitely many generalized quantifiers. Information and Computation, 123:172–184, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  36. W. F. Dowling and J. H. Gallier. Linear-time algorithms for testing the satisfiability of propositional horn formulae. Journal of Logic Programming, 1(3):267–284, 1984.

    Article  MathSciNet  MATH  Google Scholar 

  37. S. Dziembowski. Bounded-variable fixpoint queries are PSPACE-complete. In 10th Annual Conference on Computer Science Logic CSL 96, Selected papers, Lecture Notes in Computer Science, No. 1258, pages 89–105. Springer, 1996.

    Google Scholar 

  38. H. D. Ebbinghaus and J. Flum. Finite Model Theory, 2nd edition edition. Springer, 1999.

    Google Scholar 

  39. A. Ehrenfeucht and J. Mycielski. Positional strategies for mean payoff games. International Journal of Game Theory, 8:109–113, 1979.

    Article  MATH  MathSciNet  Google Scholar 

  40. A. Emerson and C. Jutla. Tree automata, mu-calculus and determinacy. In Proc. 32nd IEEE Symp. on Foundations of Computer Science, pages 368–377, 1991.

    Google Scholar 

  41. D. Epstein, J. Cannon, D. Holt, S. Levy, M. Paterson, and W. Thurston. Word Processing in Groups. Jones and Bartlett, Boston, 1992.

    MATH  Google Scholar 

  42. Yu L. Ershov, S. S. Goncharov, A. Nerode, and J. B. Remmel. Handbook of Recursive Mathematics. North-Holland, 1998.

    Google Scholar 

  43. R. Fagin. Generalised first order spectra and polynomial time recognizable sets. In R. Karp, editor, Complexity of Computation. SIAM-AMS Proceedings 7, pages 43–73, 1974.

    Google Scholar 

  44. B. Farb. Automatic groups: A guided tour. L’Enseignement Mathématique, 38:291–313, 1992.

    MathSciNet  MATH  Google Scholar 

  45. G. Gottlob, E. Grädel, and H. Veith. Datalog LITE: A deductive query language with linear time model checking. ACM Transactions on Computational Logic, 3:42–79, 2002.

    Article  Google Scholar 

  46. E. Grädel. On transitive closure logic. In Proceedings of 5th Workshop on Computer Science Logic CSL 91, Lecture Notes in Computer Science, No. 626, pages 149–163, Springer, 1991.

    Google Scholar 

  47. E. Grädel. Capturing complexity classes by fragments of second-order logic. Theoretical Computer Science, 101:35–57, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  48. E. Grädel and Y. Gurevich. Metafinite model theory. Information and Computation, 140:26–81, 1998.

    Article  MATH  MathSciNet  Google Scholar 

  49. E. Grädel, Y. Gurevich, and C. Hirsch. The complexity of query reliability, 17th ACM Symposium on Principles of Database Systems PODS 98, ACM Press, 1998.

    Google Scholar 

  50. E. Grädel and A. Malmström. 0-1 laws for recursive structures. Archive of Mathematical Logic, 38:205–215, 1999.

    Article  Google Scholar 

  51. E. Grädel and G. McColm. On the power of deterministic transitive closures. Information and Computation, 119:129–135, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  52. E. Grädel and G. McColm. Hierarchies in transitive closure logic, stratified datalog and infinitary logic. Annals of Pure and Applied Logic, 77:166–199, 1996.

    Article  Google Scholar 

  53. E. Grädel and K. Meer. Descriptive complexity theory over the real numbers. In J. Renegar, M. Shub, and S. Smale, editors, Mathematics of Numerical Analysis: Real Number Algorithms, Lectures in Applied Mathematics No. 32, pages 381–403. AMS, 1996.

    Google Scholar 

  54. E. Grädel and M. Otto. Inductive definability with counting on finite structures. Computer Science Logic, 6th Workshop, CSL ‘92, Selected Papers, Lecture Notes in Computer Science, No. 702, pages 231–247, Springer, 1993.

    Google Scholar 

  55. E. Grädel and M. Otto. On logics with two variables. Theoretical Computer Science, 224:73–113, 1999.

    Article  MATH  MathSciNet  Google Scholar 

  56. E. Grädel, W. Thomas, and T. Wilke, editors. Automata, Logics, and Infinite Games. Lecture Notes in Computer Science No. 2500. Springer, 2002.

    Google Scholar 

  57. R. Greenlaw, J. Hoover, and W. Ruzzo. Limits to Parallel Computation. P-Completeness Theory. Oxford University Press, 1995.

    Google Scholar 

  58. M. Grohe. Fixed-point logics on planar graphs. In Proc. 13th IEEE Symp. on Logic in Computer Science, pages 6–15, 1998.

    Google Scholar 

  59. M. Grohe. Isomorphism testing for embeddable graphs through definability. In Proc. 32nd ACM Symp. on Theory of Computing, pages 63–72, 2000.

    Google Scholar 

  60. M. Grohe and J. Mariño. Definability and descriptive complexity on databases of bounded tree-width. In Proceedings of ICDT 99, Lecture Notes in Computer Science, No. 1540, pages 70–82, Springer, 1999.

    Google Scholar 

  61. Y. Gurevich. Logic and the challenge of computer science. In E. Börger, editor, Current Trends in Theoretical Computer Science, pages 1–57. Computer Science Press, 1988.

    Google Scholar 

  62. Y. Gurevich and L. Harrington. Trees, automata and games. In Proceedings of the 14th Annual ACM Symposium on Theory of Computing, STOC ’82, pages 60–65, 1982.

    Google Scholar 

  63. Y. Gurevich and S. Shelah. Fixed-point extensions of first-order logic. Annals of Pure and Applied Logic, 32:265–280, 1986.

    Google Scholar 

  64. D. Harel. Towards a theory of recursive structures. In Proceedings of 23rd International Symposium on Mathematical Foundations of Computer Science MFCS 98, Lecture Notes in Computer Science, No. 1450, pages 36–53. Springer, 1998.

    Google Scholar 

  65. T. Hirst and D. Harel. More about recursive structures: Descriptive complexity and zero–one laws. In Proc. 11th IEEE Symp. on Logic in Computer Science, pages 334–348, 1996.

    Google Scholar 

  66. W. Hodges. Model Theory. Cambridge University Press, 1993.

    Google Scholar 

  67. N. Immerman. Relational queries computable in polynomial time. Information and Control, 68:86–104, 1986.

    Article  MATH  MathSciNet  Google Scholar 

  68. A. Itai and J. Makowsky. Unification as a complexity measure for logic programming. Journal of Logic Programming, 4:105–117, 1987.

    Article  MathSciNet  MATH  Google Scholar 

  69. D. Janin and I. Walukiewicz. On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic. In Proceedings of 7th International Conference on Concurrency Theory CONCUR ’96, Lecture Notes in Computer Science, No. 1119, pages 263–277. Springer, 1996.

    Google Scholar 

  70. N. Jones and W. Laaser. Complete problems for deterministic polynomial time. Theoretical Computer Science, 3:105–117, 1977.

    Article  MATH  MathSciNet  Google Scholar 

  71. N. Jones and A. Selman. Turing machines and the spectra of first-order formulas. Journal of Symbolic Logic, 39:139–150, 1974.

    Article  MATH  MathSciNet  Google Scholar 

  72. M. Jurdziński. Deciding the winner in parity games is in UP ⋒ Co-UP. Information Processing Letters, 68:119–124, 1998.

    Article  MathSciNet  Google Scholar 

  73. M. Jurdziński. Small progress measures for solving parity games. In STACS 2000, 17th Annual Symposium on Theoretical Aspects of Computer Science, Proceedings, Lecture Notes in Computer Science, No. 1770, pages 290–301. Springer, 2000.

    Google Scholar 

  74. P. Kanellakis, G. Kuper, and P. Revesz. Constraint query languages. Journal of Computer and Systems Sciences, 51:26–52, 1995.

    Article  MathSciNet  Google Scholar 

  75. B. Khoussainov and A. Nerode. Automatic presentations of structures. In LCC ’94: Selected Papers from the International Workshop on Logical and Computational Complexity, Lecture Notes in Computer Science, No. 960, pages 367–392. Springer, 1995.

    Google Scholar 

  76. B. Khoussainov, S. Rubin, and F. Stephan. On automatic partial orders. Proceedings of 18th Annual IEEE Symposium on Logic in Computer Science, LICS 03, pages 168–177, 2003.

    Google Scholar 

  77. B. Khoussainov, A. Nies, S. Rubin, and F. Stephan. Automatic structures: Richness and limitations. Proceedings of 19th Annual IEEE Symposium on Logic in Computer Science, LICS 04, pages 44–53, 2004.

    Google Scholar 

  78. B. Khoussainov, S. Rubin, and F. Stephan. Definability and regularity in automatic structures. In Proceedings of STACS 04, pages 440–451, 2004.

    Google Scholar 

  79. P. Kolaitis. The expressive power of stratified logic programs. Information and Computation, 90:50–66, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  80. S. Kreutzer. Expressive equivalence of least and inflationary fixed point logic. In Proceedings of 17th IEEE Symp. on Logic in Computer Science LICS02, pages 403–410, 2002.

    Google Scholar 

  81. G. uper, L. Libkin, and J. Paredaens, editors. Constraint Databases. Springer, 2000.

    Google Scholar 

  82. D. Martin. Borel determinacy. Annals of Mathematics, 102:336–371, 1975.

    Article  Google Scholar 

  83. Y. Matijasevich. Hilbert’s Tenth Problem. MIT Press, 1993.

    Google Scholar 

  84. K. Meer. Query languages for real number databases based on descriptive complexity over R. In Proc. 24th International Symposium on Mathematical Foundations of Computer Science MFCS 99, Lecture Notes in Computer Science Nr. 1672, pages 12–22. Springer, 1999.

    Google Scholar 

  85. Y. Moschovakis. Elementary Induction on Abstract Structures. North-Holland, 1974.

    Google Scholar 

  86. A. Mostowski. Games with forbidden positions. Technical Report 78, University of Gdansk, 1991.

    Google Scholar 

  87. D. Muller and P. Schupp. Groups, the theory of ends, and context-free languages. Journal of Computer and System Sciences, 26:295–310, 1983.

    Article  MATH  MathSciNet  Google Scholar 

  88. D. Muller and P. Schupp. The theory of ends, pushdown automata, and second-order logic. Theoretical Computer Science, 37:51–75, 1985.

    Article  MATH  MathSciNet  Google Scholar 

  89. M. Otto. Bounded Variable Logics and Counting. Springer, 1997.

    Google Scholar 

  90. M. Otto. Bisimulation-invariant Ptime and higher-dimensional mu-calculus. Theoretical Computer Science, 224:237–265, 1999.

    Article  MATH  MathSciNet  Google Scholar 

  91. C. Papadimitriou. A note on the expressive power of Prolog. Bulletin of the EATCS, 26:21–23, 1985.

    MathSciNet  Google Scholar 

  92. S. Rubin. Automatic Structures. PhD thesis, University of Auckland, New Zealand, 2004.

    Google Scholar 

  93. H. Scholz. Ein ungelöstes Problem in der symbolischen Logik. Journal of Symbolic Logic, 17:160, 1952.

    Google Scholar 

  94. A. Stolboushkin. Towards recursive model theory. In J. Makowsky and E. Ravve, editors, Logic Colloquium 95,Lecture Notes in Logic, No. 11, pages 325–338. Springer, 1998.

    Google Scholar 

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

    MATH  Google Scholar 

  96. W. Thomas. On the synthesis of strategies in infinite games. In Proceedings of STACS 95, Lecture Notes in Computer Science,No. 900, pages 1–13. Springer, 1995.

    Google Scholar 

  97. W. Thomas. Languages, automata, and logic. In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Languages Vol. 3, pages 389–455. Springer, 1997.

    Google Scholar 

  98. W. Thomas. Constructing infinite graphs with a decidable MSO-theory. In Proceedings of the 28th International Symposium on Mathematical Foundations of Computer Science MFCS 03, Lecture Notes in Computer Science, No. 2747, pages 113-124, Springer, 2003.

    Google Scholar 

  99. M. Vardi. The complexity of relational query languages. In Proceedings of the 14th ACM Symposium on the Theory of Computing, pages 137–146, 1982.

    Google Scholar 

  100. M. Vardi. On the complexity of bounded-variable queries. In Proc. 14th ACM Symp. on Principles of Database Systems, pages 266–267, 1995.

    Google Scholar 

  101. I. Walukiewicz. Monadic second-order logic on tree-like structures. Theoretical Computer Science, 275:311–346, 2001.

    Article  MathSciNet  Google Scholar 

  102. W. Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science, 200:135–183, 1998.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Grädel, E. (2007). Finite Model Theory and Descriptive Complexity. In: Finite Model Theory and Its Applications. Texts in Theoretical Computer Science an EATCS Series. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-68804-8_3

Download citation

  • DOI: https://doi.org/10.1007/3-540-68804-8_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00428-8

  • Online ISBN: 978-3-540-68804-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics