nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

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

verfasst von : Kamal Lodaya, A. V. Sreejith

Erschienen in: Developments in Language Theory

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel The Generalized Rank of Trace Languages

Nächstes Kapitel Deleting Deterministic Restarting Automata with Two Windows

Barrington, D.A.M., Immerman, N., Straubing, H.: On uniformity within \(NC^1\). J. Comp. Syst. Sci. 41(3), 274–306 (1990)MathSciNetCrossRefMATH

Büchi, J.R.: Weak second-order arithmetic and finite automata. Z. Math. Logik Grundl. Math. 6, 66–92 (1960)MathSciNetCrossRefMATH

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)MathSciNetCrossRefMATH

van Emde Boas, P.: The convenience of tilings. In: Sorbi, A. (ed.) Complexity, Logic and Recursion Theory, pp. 331–363. CRC Press (1997)

Etessami, K., Vardi, M.Y., Wilke, T.: First-order logic with two variables and unary temporal logic. Inf. Comput. 179(2), 279–295 (2002)MathSciNetCrossRefMATH

Grädel, E., Otto, M., Rosen, E.: Undecidability results on two-variable logics. Arch. Math. Log. 38, 213–354 (1999)MathSciNetMATH

Krebs, A.: Typed semigroups, majority logic, and threshold circuits. Ph.D. thesis, Universität Tübingen (2008)

Krebs, A., Lodaya, K., Pandya, P., Straubing, H.: Two-variable logic with a between relation. In: Proceeding of 31st LICS (2016)

Lautemann, C., McKenzie, P., Schwentick, T., Vollmer, H.: The descriptive complexity approach to LOGCFL. J. Comp. Syst. Sci. 62(4), 629–652 (2001)MathSciNetCrossRefMATH

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 CrossRef

11.

Manuel, A., Sreejith, A.: Two-variable logic over countable linear orderings. In: 41st MFCS, Kraków, pp. 66:1–66:13 (2016)

12.

Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall, New Jersy (1967)MATH

13.

Pacholski, L., Szwast, W., Tendera, L.: Complexity of two-variable logic with counting. In: 12th LICS, Warsaw, pp. 318–327. IEEE (1997)

14.

Paris, J., Wilkie, A.: Counting \(\Delta _0\) sets. Fundam. Math. 127, 67–76 (1986)MATH

15.

Robinson, R.M.: Restricted set-theoretical definitions in arithmetic. Proc. Am. Math. Soc. 9, 238–242 (1958)MathSciNetCrossRefMATH

16.

Schweikardt, N.: Arithmetic, first-order logic, and counting quantifiers. ACM Trans. Comput. Log. 6(3), 634–671 (2005)MathSciNetCrossRefMATH

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 CrossRef

18.

Sreejith, A.V.: Expressive completeness for LTL with modulo counting and group quantifiers. Electr. Notes Theor. Comput. Sci. 278, 201–214 (2011)MathSciNetCrossRefMATH

19.

Sreejith, A.V.: Regular quantifiers in logics. Ph.D. thesis, HBNI (2013)

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)MathSciNetCrossRefMATH

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)MathSciNetCrossRefMATH

22.

Straubing, H., Thérien, D., Thomas, W.: Regular languages defined with generalized quantifiers. Inf. Comput. 118(3), 389–301 (1995)MathSciNetMATH

23.

Tesson, P., Thérien, D.: Logic meets algebra: the case of regular languages. Log. Meth. Comp. Sci. 3(1), 1–26 (2007)MathSciNetMATH

24.

Thomas, W.: Classifying regular events in symbolic logic. J. Comput. Syst. Sci. 25(3), 360–376 (1982)MathSciNetCrossRefMATH

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)CrossRef

26.

Weis, P., Immerman, N.: Structure theorem and strict alternation hierarchy for FO² 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 CrossRef

Titel: Two-Variable First Order Logic with Counting Quantifiers: Complexity Results
verfasst von: Kamal Lodaya
A. V. Sreejith
Verlag: Springer International Publishing
Buch: Developments in Language Theory
Print ISBN: 978-3-319-62808-0

Electronic ISBN: 978-3-319-62809-7

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-62809-7_19

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"