Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Block Products and Nesting Negations in FO2

  • Conference paper
Computer Science - Theory and Applications (CSR 2014)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8476))

Included in the following conference series:

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.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight 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.

Similar content being viewed by others

References

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

    Article  MATH  MathSciNet  Google Scholar 

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

    MATH  MathSciNet  Google Scholar 

  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)

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  6. Glaßer, C., Schmitz, H.: Languages of dot-depth 3/2. Theory of Computing Systems 42(2), 256–286 (2008)

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

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

    MATH  MathSciNet  Google Scholar 

  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. 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. Kufleitner, M., Lauser, A.: Around dot-depth one. Int. J. Found. Comput. Sci. 23(6), 1323–1339 (2012)

    Article  MATH  MathSciNet  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. 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. 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. Kufleitner, M., Weil, P.: On logical hierarchies within FO2-definable languages. Log. Methods Comput. Sci. 8, 1–30 (2012)

    MathSciNet  Google Scholar 

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

    Google Scholar 

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

    MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. Straubing, H.: A generalization of the Schützenberger product of finite monoids. Theor. Comput. Sci. 13, 137–150 (1981)

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

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

    Chapter  Google Scholar 

  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. Thérien, D.: Classification of finite monoids: The language approach. Theor. Comput. Sci. 14(2), 195–208 (1981)

    Article  MATH  Google Scholar 

  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. Thomas, W.: Classifying regular events in symbolic logic. J. Comput. Syst. Sci. 25, 360–376 (1982)

    Article  MATH  Google Scholar 

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

    Google Scholar 

  33. Weis, P., Immerman, N.: Structure theorem and strict alternation hierarchy for FO2 on words. Log. Methods Comput. Sci. 5, 1–23 (2009)

    MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Formale Methoden der Informatik, Universität Stuttgart, Germany

    Lukas Fleischer, Manfred Kufleitner & Alexander Lauser

  2. Fakultät für Informatik, Technische Universität München, Germany

    Manfred Kufleitner

Authors
  1. Lukas Fleischer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Manfred Kufleitner
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alexander Lauser
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Steklov Institute of Mathematics at St. Petersburg, Russian Academy of Sciences, 27 Fontanka,, 191023, St. Petersburg, Russia

    Edward A. Hirsch

  2. Higher School of Economics, National Research University, 109028, Moscow, Russia

    Sergei O. Kuznetsov

  3. CNRS and University Paris Diderot, Paris, France

    Jean-Éric Pin

  4. Moscow State University, 119992, Moscow, Russia

    Nikolay K. Vereshchagin

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Fleischer, L., Kufleitner, M., Lauser, A. (2014). Block Products and Nesting Negations in FO2 . In: Hirsch, E.A., Kuznetsov, S.O., Pin, JÉ., Vereshchagin, N.K. (eds) Computer Science - Theory and Applications. CSR 2014. Lecture Notes in Computer Science, vol 8476. Springer, Cham. https://doi.org/10.1007/978-3-319-06686-8_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-06686-8_14

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-06685-1

  • Online ISBN: 978-3-319-06686-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation