Two-Variable First Order Logic with Counting Quantifiers: Complexity Results

  • Kamal Lodaya
  • A. V. SreejithEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10396)


Etessami et al. [5] showed that satisfiability of two-variable first order logic \(\mathrm {FO}^2\)[<] on word models is Nexptime-complete. We extend this upper bound to the slightly stronger logic \(\mathrm {FO}^2\)[\(<,succ ,\equiv \)], which allows checking whether a word position is congruent to r modulo q, for some divisor q and remainder r. If we allow the more powerful modulo counting quantifiers of Straubing, Thérien et al. [22] (we call this two-variable fragment FOmod \(^2\)[\(<,succ \)]), satisfiability becomes Expspace-complete. A more general counting quantifier, FOunC\(^2\)[\(<,succ \)], makes the logic undecidable.



We would like to thank four DLT referees and the DLT program committee for their suggestions to improve this paper.


  1. 1.
    Barrington, D.A.M., Immerman, N., Straubing, H.: On uniformity within \(NC^1\). J. Comp. Syst. Sci. 41(3), 274–306 (1990)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Büchi, J.R.: Weak second-order arithmetic and finite automata. Z. Math. Logik Grundl. Math. 6, 66–92 (1960)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Cai, J., Fürer, M., Immerman, N.: An optimal lower bound on the number of variables for graph identification. Combinatorica 12(4), 389–410 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    van Emde Boas, P.: The convenience of tilings. In: Sorbi, A. (ed.) Complexity, Logic and Recursion Theory, pp. 331–363. CRC Press (1997)Google Scholar
  5. 5.
    Etessami, K., Vardi, M.Y., Wilke, T.: First-order logic with two variables and unary temporal logic. Inf. Comput. 179(2), 279–295 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Grädel, E., Otto, M., Rosen, E.: Undecidability results on two-variable logics. Arch. Math. Log. 38, 213–354 (1999)MathSciNetzbMATHGoogle Scholar
  7. 7.
    Krebs, A.: Typed semigroups, majority logic, and threshold circuits. Ph.D. thesis, Universität Tübingen (2008)Google Scholar
  8. 8.
    Krebs, A., Lodaya, K., Pandya, P., Straubing, H.: Two-variable logic with a between relation. In: Proceeding of 31st LICS (2016)Google Scholar
  9. 9.
    Lautemann, C., McKenzie, P., Schwentick, T., Vollmer, H.: The descriptive complexity approach to LOGCFL. J. Comp. Syst. Sci. 62(4), 629–652 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Lodaya, K., Sreejith, A.V.: LTL can be more succinct. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol. 6252, pp. 245–258. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-15643-4_19 CrossRefGoogle Scholar
  11. 11.
    Manuel, A., Sreejith, A.: Two-variable logic over countable linear orderings. In: 41st MFCS, Kraków, pp. 66:1–66:13 (2016)Google Scholar
  12. 12.
    Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall, New Jersy (1967)zbMATHGoogle Scholar
  13. 13.
    Pacholski, L., Szwast, W., Tendera, L.: Complexity of two-variable logic with counting. In: 12th LICS, Warsaw, pp. 318–327. IEEE (1997)Google Scholar
  14. 14.
    Paris, J., Wilkie, A.: Counting \(\Delta _0\) sets. Fundam. Math. 127, 67–76 (1986)zbMATHGoogle Scholar
  15. 15.
    Robinson, R.M.: Restricted set-theoretical definitions in arithmetic. Proc. Am. Math. Soc. 9, 238–242 (1958)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Schweikardt, N.: Arithmetic, first-order logic, and counting quantifiers. ACM Trans. Comput. Log. 6(3), 634–671 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Schwentick, T., Thérien, D., Vollmer, H.: Partially-ordered two-way automata: A new characterization of DA. In: Kuich, W., Rozenberg, G., Salomaa, A. (eds.) DLT 2001. LNCS, vol. 2295, pp. 239–250. Springer, Heidelberg (2002). doi: 10.1007/3-540-46011-X_20 CrossRefGoogle Scholar
  18. 18.
    Sreejith, A.V.: Expressive completeness for LTL with modulo counting and group quantifiers. Electr. Notes Theor. Comput. Sci. 278, 201–214 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Sreejith, A.V.: Regular quantifiers in logics. Ph.D. thesis, HBNI (2013)Google Scholar
  20. 20.
    Straubing, H., Tesson, P., Thérien, D.: Weakly iterated block products and applications to logic and complexity. Int. J. Alg. Comput. 20(2), 319–341 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Straubing, H., Thérien, D.: Regular languages defined by generalized first-order formulas with a bounded number of bound variables. Theor. Comput. Syst. 36(1), 29–69 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Straubing, H., Thérien, D., Thomas, W.: Regular languages defined with generalized quantifiers. Inf. Comput. 118(3), 389–301 (1995)MathSciNetzbMATHGoogle Scholar
  23. 23.
    Tesson, P., Thérien, D.: Logic meets algebra: the case of regular languages. Log. Meth. Comp. Sci. 3(1), 1–26 (2007)MathSciNetzbMATHGoogle Scholar
  24. 24.
    Thomas, W.: Classifying regular events in symbolic logic. J. Comput. Syst. Sci. 25(3), 360–376 (1982)MathSciNetCrossRefzbMATHGoogle Scholar
  25. 25.
    Thomas, W.: Languages, automata and logic. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Language Theory, vol. III, pp. 389–455. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  26. 26.
    Weis, P., Immerman, N.: Structure theorem and strict alternation hierarchy for FO2 on words. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 343–357. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-74915-8_27 CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.The Institute of Mathematical SciencesCIT CampusChennaiIndia
  2. 2.Chennai Mathematical InstituteSiruseri, KelambakkamIndia

Personalised recommendations