# Block Products and Nesting Negations in FO2

• Lukas Fleischer
• Manfred Kufleitner
• Alexander Lauser
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8476)

## Abstract

The alternation hierarchy in two-variable first-order logic FO2[ < ] over words was recently shown to be decidable by Kufleitner and Weil, and independently by Krebs and Straubing. In this paper 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 FO2 is defined by disallowing universal quantifiers and having at most m − 1 nested negations. One can view $$\Sigma^2_m$$ as the formulas in FO2 which have at most m blocks of quantifiers on every path of their parse tree, and the first block is existential. Thus, the m th level of the FO2-alternation hierarchy is the Boolean closure of $$\Sigma^2_m$$. 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 by a two-variable first-order formula with negation nesting depth at most m. More precisely, for every m we give ω-terms U m and V m such that an FO2-definable language is in $$\Sigma^2_m$$ if and only if its ordered syntactic monoid satisfies the identity U m  ≤ V m . Among other techniques, the proof relies on an extension of block products to ordered monoids.

## Keywords

regular language finite monoid positive variety first-order logic

## References

1. 1.
Büchi, J.R.: Weak second-order arithmetic and finite automata. Z. Math. Logik Grundlagen Math. 6, 66–92 (1960)
2. 2.
Cohen, R.S., Brzozowski, J.A.: Dot-depth of star-free events. J. Comput. Syst. Sci. 5(1), 1–16 (1971)
3. 3.
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)
4. 4.
Ebbinghaus, H.-D., Flum, J.: Finite Model Theory. In: Perspectives in Mathematical Logic. Springer (1995)Google Scholar
5. 5.
Elgot, C.C.: Decision problems of finite automata design and related arithmetics. Trans. Amer. Math. Soc. 98, 21–51 (1961)
6. 6.
Glaßer, C., Schmitz, H.: Languages of dot-depth 3/2. Theory of Computing Systems 42(2), 256–286 (2008)
7. 7.
Kamp, J.A.W.: Tense Logic and the Theory of Linear Order. PhD thesis, University of California (1968)Google Scholar
8. 8.
Knast, R.: A semigroup characterization of dot-depth one languages. RAIRO, Inf. Théor. 17(4), 321–330 (1983)
9. 9.
Krebs, A., Straubing, H.: An effective characterization of the alternation hierarchy in two-variable logic. In: FSTTCS 2012, Proceedings. LIPIcs, vol. 18, pp. 86–98. Dagstuhl Publishing (2012)Google Scholar
10. 10.
Kufleitner, M., Lauser, A.: Languages of dot-depth one over infinite words. In: Proceedings of LICS 2011, pp. 23–32. IEEE Computer Society (2011)Google Scholar
11. 11.
Kufleitner, M., Lauser, A.: Around dot-depth one. Int. J. Found. Comput. Sci. 23(6), 1323–1339 (2012)
12. 12.
Kufleitner, M., Lauser, A.: The join levels of the trotter-weil hierarchy are decidable. In: Rovan, B., Sassone, V., Widmayer, P. (eds.) MFCS 2012. LNCS, vol. 7464, pp. 603–614. Springer, Heidelberg (2012)
13. 13.
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)Google Scholar
14. 14.
Kufleitner, M., Lauser, A.: Quantifier alternation in two-variable first-order logic with successor is decidable. In: Proceedings of STACS 2013. LIPIcs, vol. 20, pp. 305–316. Dagstuhl Publishing (2013)Google Scholar
15. 15.
Kufleitner, M., Weil, P.: The FO2 alternation hierarchy is decidable. In: Proceedings of CSL 2012. LIPIcs, vol. 16, pp. 426–439. Dagstuhl Publishing (2012)Google Scholar
16. 16.
Kufleitner, M., Weil, P.: On logical hierarchies within FO2-definable languages. Log. Methods Comput. Sci. 8, 1–30 (2012)
17. 17.
McNaughton, R., Papert, S.: Counter-Free Automata. The MIT Press (1971)Google Scholar
18. 18.
Pin, J.-É.: A variety theorem without complementation. Russian Mathematics (Iz. VUZ) 39, 80–90 (1995)
19. 19.
Pin, J.-É., Weil, P.: Polynomial closure and unambiguous product. Theory Comput. Syst. 30(4), 383–422 (1997)
20. 20.
Pin, J.-É., Weil, P.: The wreath product principle for ordered semigroups. Commun. Algebra 30(12), 5677–5713 (2002)
21. 21.
Schützenberger, M.P.: On finite monoids having only trivial subgroups. Inf. Control 8, 190–194 (1965)
22. 22.
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)
23. 23.
Simon, I.: Piecewise testable events. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 214–222. Springer, Heidelberg (1975)Google Scholar
24. 24.
Straubing, H.: A generalization of the Schützenberger product of finite monoids. Theor. Comput. Sci. 13, 137–150 (1981)
25. 25.
Straubing, H.: Finite Automata, Formal Logic, and Circuit Complexity. Birkhäuser (1994)Google Scholar
26. 26.
Straubing, H.: Algebraic characterization of the alternation hierarchy in FO2[ < ] on finite words. In: Proceedings CSL 2011. LIPIcs, vol. 12, pp. 525–537. Dagstuhl Publishing (2011)Google Scholar
27. 27.
Straubing, H., Thérien, D.: Weakly iterated block products of finite monoids. In: Rajsbaum, S. (ed.) LATIN 2002. LNCS, vol. 2286, pp. 91–104. Springer, Heidelberg (2002)
28. 28.
Tesson, P., Thérien, D.: Diamonds are forever: The variety DA. In: Proceedings of Semigroups, Algorithms, Automata and Languages, pp. 475–500. World Scientific (2002)Google Scholar
29. 29.
Thérien, D.: Classification of finite monoids: The language approach. Theor. Comput. Sci. 14(2), 195–208 (1981)
30. 30.
Thérien, D.: Th. Wilke. Over words, two variables are as powerful as one quantifier alternation. In: Proceedings of STOC 1998, pp. 234–240. ACM Press (1998)Google Scholar
31. 31.
Thomas, W.: Classifying regular events in symbolic logic. J. Comput. Syst. Sci. 25, 360–376 (1982)
32. 32.
Trakhtenbrot, B.A.: Finite automata and logic of monadic predicates (in Russian). Dokl. Akad. Nauk. SSSR 140, 326–329 (1961)Google Scholar
33. 33.
Weis, P., Immerman, N.: Structure theorem and strict alternation hierarchy for FO2 on words. Log. Methods Comput. Sci. 5, 1–23 (2009)

© Springer International Publishing Switzerland 2014

## Authors and Affiliations

• Lukas Fleischer
• 1
• Manfred Kufleitner
• 1
• 2
• Alexander Lauser
• 1
1. 1.Formale Methoden der InformatikUniversität StuttgartGermany
2. 2.Fakultät für InformatikTechnische Universität MünchenGermany
{"ft_lang_label":"__label__en","ft_lang_prob":0.5149516,"math_prob":0.5618416,"size":6779,"snap":"2020-24-2020-29","text_gpt3_token_len":2104,"char_repetition_ratio":0.15099631,"word_repetition_ratio":0.0151024815,"special_character_ratio":0.30609235,"punctuation_ratio":0.2968961,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.974908,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2020-07-04T00:34:27Z\",\"WARC-Record-ID\":\"<urn:uuid:2672c291-f222-4fce-8b8c-ffa6f805b969>\",\"Content-Length\":\"98690\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:c45b6473-cbbc-4575-b1b7-857b844735ce>\",\"WARC-Concurrent-To\":\"<urn:uuid:be0c8b79-7ce1-4ba0-af59-3e0120ba7210>\",\"WARC-IP-Address\":\"199.232.64.95\",\"WARC-Target-URI\":\"https://link.springer.com/chapter/10.1007/978-3-319-06686-8_14\",\"WARC-Payload-Digest\":\"sha1:WQZRA6QSRZNHWM33DSIDUTQDDRYCIQSC\",\"WARC-Block-Digest\":\"sha1:QLLRF7GV2ANXSRY5624XGE32DARAYWLJ\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2020/CC-MAIN-2020-29/CC-MAIN-2020-29_segments_1593655883439.15_warc_CC-MAIN-20200703215640-20200704005640-00226.warc.gz\"}"}