Top

Theory of Computing Systems

Published in:

01-10-2016

The Half-Levels of the FO₂ Alternation Hierarchy

Authors: Lukas Fleischer, Manfred Kufleitner, Alexander Lauser

Published in: Theory of Computing Systems | Issue 2/2017

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

The alternation hierarchy in two-variable first-order logic FO²[<] over words was shown to be decidable by Kufleitner and Weil, and independently by Krebs and Straubing. We consider a similar hierarchy, reminiscent of the half levels of the dot-depth hierarchy or the Straubing-Thérien hierarchy. The fragment \({{\Sigma }^{2}_{m}}\) of FO² is defined by disallowing universal quantifiers and having at most m−1 nested negations. The Boolean closure of \({{\Sigma }^{2}_{m}}\) yields the m ^th level of the FO²-alternation hierarchy. We give an effective characterization of \({{\Sigma }^{2}_{m}}\), i.e., for every integer m one can decide whether a given regular language is definable in \({{\Sigma }^{2}_{m}}\). Among other techniques, the proof relies on an extension of block products to ordered monoids.

previous article Processing Succinct Matrices and Vectors

next article Separation Logic with One Quantified Variable

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

Almeida, J., Weil, P.: Profinite categories and semidirect products. J. Pure Appl. Algebra 123(1–3), 1–50 (1998)MathSciNetCrossRefMATH

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

Cohen, R.S., Brzozowski, J.A.: Dot-depth of star-free events. J. Comput. Syst. Sci. 5(1), 1–16 (1971)MathSciNetCrossRefMATH

Diekert, V., Gastin, P., Kufleitner, M.: A survey on small fragments of first-order logic over finite words. Int. J. Found. Comput. Sci. 19(3), 513–548 (2008)MathSciNetCrossRefMATH

Ebbinghaus, H.-D., Flum, J.: Finite Model Theory. Perspectives in Mathematical Logic. Springer (1995)

Eilenberg, S.: Automata, Languages, and Machines, vol. B. Academic Press, New York and London (1976)

Elgot, C.C.: Decision problems of finite automata design and related arithmetics. Trans. Amer. Math. Soc. 98, 21–51 (1961)MathSciNetCrossRefMATH

Fleischer, L., Kufleitner, M., Lauser, A.: Block products and nesting negations in FO ². In: Proceedings of CSR 2014 of LNCS, vol. 8476, p 2014. Springer

Glaßer, Ch., Schmitz, H.: Languages of dot-depth 3/2. Theory Comput. Syst. 42(2), 256–286 (2008)MathSciNetCrossRefMATH

10.

Kamp, J.A.W.: Tense Logic and the Theory of Linear Order. PhD thesis, University of California (1968)

11.

Knast, R.: A semigroup characterization of dot-depth one languages. RAIRO, Inf. Théor. 17(4), 321–330 (1983)MathSciNetCrossRefMATH

12.

Krebs, A., Straubing, H.: An effective characterization of the alternation hierarchy in two-variable logic. In: Proceedings of FSTTCS 2012 of LIPIcs, vol. 18, p 2012. Dagstuhl Publishing

13.

Kufleitner, M., Lauser, A.: Languages of dot-depth one over infinite words. In: Proceedings of LICS 2011, pp 23–32. IEEE Computer Society (2011)

14.

Kufleitner, M., Lauser, A.: Around dot-depth one. Int. J. Comput. Sci. 23 (6), 1323–1339 (2012)MathSciNetMATH

15.

Kufleitner, M., Lauser, A.: The join levels of the Trotter-Weil hierarchy are decidable. In: Proceedings of MFCS 2012 of LNCS, vol. 7464, pp 603–614. Springer (2012)

16.

Kufleitner, M., Lauser, A.: The join of the varieties of R-trivial and L-trivial monoids via combinatorics on words. Discrete Math. Theor. Comput. Sci. 14(1), 141–146 (2012)MathSciNetMATH

17.

Kufleitner, M., Lauser, A.: Quantifier alternation in two-variable first-order logic with successor is decidable. In: Proceedings of STACS 2013 of LIPIcs, vol. 20, p 2013. Dagstuhl Publishing

18.

Kufleitner, M., Weil, P.: The FO² alternation hierarchy is decidable. In: Proceedings of CSL 2012 of LIPIcs, vol. 16, pp 426–439. Dagstuhl Publishing (2012)

19.

McNaughton, R., Papert, S.: Counter-Free Automata. The MIT Press (1971)

20.

Pin, J.-É.: A variety theorem without complementation. In: Russian Mathematics (Iz. VUZ), vol. 39, pp 80–90 (1995)

21.

Pin, J.-É., Weil, P.: Polynomial closure and unambiguous product. Theory Comput. Syst. 30(4), 383–422 (1997)MathSciNetCrossRefMATH

22.

Pin, J.-É., Weil, P.: Semidirect products of ordered semigroups. Commun. Algebra 30(1), 149–169 (2002)MathSciNetCrossRefMATH

23.

Pin, J.-É., Weil, P.: The wreath product principle for ordered semigroups. Commun. Algebra 30(12), 5677–5713 (2002)MathSciNetCrossRefMATH

24.

Place, Th., Zeitoun, M.: Going higher in the first-order quantifier alternation hierarchy on words. In: Proceedings of ICALP 2014 of LNCS, vol. 8573, pp 342–353. Springer (2014)

25.

Rhodes, J., Tilson, B.: The kernel of monoid morphisms. J. Pure Appl. Algebra 62(3), 227–268 (1989)MathSciNetCrossRefMATH

26.

Rhodes, J., Weil, P.: Decomposition techniques for finite semigroups, using categories II. J. Pure Appl. Algebra 62(3), 285–312 (1989)MathSciNetCrossRefMATH

27.

Schützenberger, M.P.: On finite monoids having only trivial subgroups. Inf. Control 8, 190–194 (1965)MathSciNetCrossRefMATH

28.

Schwentick, Th., Thérien, D., Vollmer, H.: Partially-ordered two-way automata: A new characterization of DA. In: Proceedings of DLT 2001 of LNCS, vol. 2295, pp 239–250. Springer (2002)

29.

Simon, I.: Piecewise testable events. In: 2nd GI Conference of Automation, Theoretical Formation Languages of LNCS, vol. 33, pp 214–222. Springer (1975)

30.

Straubing, H.: Families of recognizable sets corresponding to certain varieties of finite monoids. J. Pure Appl. Algebra 15(3), 305–318 (1979)MathSciNetCrossRefMATH

31.

Straubing, H.: Aperiodic homomorphisms and the concatenation product of recognizable sets. J. Pure Appl. Algebra 15(3), 319–327 (1979)MathSciNetCrossRefMATH

32.

Straubing, H.: A generalization of the Schützenberger product of finite monoids. Theor. Comput. Sci. 13, 137–150 (1981)CrossRefMATH

33.

Straubing, H.: Finite semigroup varieties of the form V∗D. J. Pure Appl. Algebra 36(1), 53–94 (1985)MathSciNetCrossRefMATH

34.

Straubing, H.: Finite Automata, Formal Logic, and Circuit Complexity. Birkhäuser (1994)

35.

Straubing, H.: Algebraic characterization of the alternation hierarchy in FO²[<] on finite words. In: Proceedings of CSL 2011 of LIPIcs, vol. 12, pp 525–537. Dagstuhl Publishing (2011)

36.

Tesson, P., Thérien, D.: Diamonds are forever: The variety DA. In: Proceedings of Semigroups, Algorithms, Automata and Languages 2001, pp 475–500. World Scientific (2002)

37.

Thérien, D.: Classification of finite monoids: The language approach. Theor. Comput. Sci. 14(2), 195–208 (1981)MathSciNetCrossRefMATH

38.

Thérien, D.: Two-sided wreath product of categories. J. Pure Appl. Algebra 74(3), 307–315 (1991)MathSciNetCrossRefMATH

39.

Thérien, D., Wilke, Th.: Over words, two variables are as powerful as one quantifier alternation. In: Proceedings of STOC 1998, pp 234–240. ACM Press (1998)

40.

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

41.

Trakhtenbrot, B.A.: Finite automata and logic of monadic predicates. Dokl. Akad. Nauk SSSR 140, 326–329 (1961). in Russian

42.

Weil, P.: Closure of varieties of languages under products with counter. J. Comput. Syst. Sci. 45(3), 316–339 (1992)MathSciNetCrossRefMATH

43.

Weis, Ph., Immerman, N.: Structure theorem and strict alternation hierarchy for FO² on words. Log. Methods Comput. Sci. 5(3), 1–23 (2009)MathSciNetCrossRefMATH

Title: The Half-Levels of the FO2 Alternation Hierarchy
Authors: Lukas Fleischer
Manfred Kufleitner
Alexander Lauser
Publication date: 01-10-2016
Publisher: Springer US
Published in: Theory of Computing Systems / Issue 2/2017
Print ISSN: 1432-4350
Electronic ISSN: 1433-0490
DOI: https://doi.org/10.1007/s00224-016-9712-2

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Other articles of this Issue 2/2017

Separation Logic with One Quantified Variable

Equations Over Free Inverse Monoids with Idempotent Variables

Preface

Generalized LR Parsing Algorithm for Grammars with One-Sided Contexts

Space Saving by Dynamic Algebraization Based on Tree-Depth

On the Satisfiability of Quantum Circuits of Small Treewidth

Premium Partner