Document Open Access Logo

Modulo Counting on Words and Trees

Authors Bartosz Bednarczyk, Witold Charatonik

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2017.12.pdf
  • Filesize: 0.62 MB
  • 16 pages

Document Identifiers

Subject Classification

Keywords
  • satisfiability
  • trees
  • words
  • two-variable logic
  • modulo quantifiers

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We consider the satisfiability problem for the two-variable fragment of the first-order logic extended with modulo counting quantifiers and interpreted over finite words or trees. We prove a small-model property of this logic, which gives a technique for deciding the satisfiability problem. In the case of words this gives a new proof of EXPSPACE upper bound, and in the case of trees it gives a 2EXPTIME algorithm. This algorithm is optimal: we prove a matching lower bound by a generic reduction from alternating Turing machines working in exponential space; the reduction involves a development of a new version of tiling games.

Cite As Get BibTex

Bartosz Bednarczyk and Witold Charatonik. Modulo Counting on Words and Trees. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.FSTTCS.2017.12

Author Details

Bartosz Bednarczyk
Witold Charatonik

References

  1. Augustin Baziramwabo, Pierre McKenzie, and Denis Thérien. Modular temporal logic. In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999, pages 344-351. IEEE Computer Society, 1999. URL: http://dx.doi.org/10.1109/LICS.1999.782629.
  2. Bartosz Bednarczyk and Witold Charatonik. Modulo counting on words and trees. CoRR, http://arxiv.org/abs/1710.05582, 2017.
  3. Bartosz Bednarczyk, Witold Charatonik, and Emanuel Kieronski. Extending two-variable logic on trees. In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual Conference on Computer Science Logic, CSL 2017, August 20-24, 2017, Stockholm, Sweden, volume 82 of LIPIcs, pages 11:1-11:20. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2017.11.
  4. Saguy Benaim, Michael Benedikt, Witold Charatonik, Emanuel Kieroński, Rastislav Lenhardt, Filip Mazowiecki, and James Worrell. Complexity of two-variable logic on finite trees. ACM Transactions on Computational Logic, 17(4):32:1-32:38, 2017. Extended abstract in ICALP 2013. URL: http://dl.acm.org/citation.cfm?id=2996796.
  5. Michael Benedikt and Luc Segoufin. Regular tree languages definable in FO and in fo_mod. ACM Trans. Comput. Log., 11(1):4:1-4:32, 2009. URL: http://dx.doi.org/10.1145/1614431.1614435.
  6. Christoph Berkholz, Jens Keppeler, and Nicole Schweikardt. Answering FO+MOD queries under updates on bounded degree databases. In Michael Benedikt and Giorgio Orsi, editors, 20th International Conference on Database Theory, ICDT 2017, March 21-24, 2017, Venice, Italy, volume 68 of LIPIcs, pages 8:1-8:18. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.ICDT.2017.8.
  7. Witold Charatonik and Piotr Witkowski. Two-variable logic with counting and a linear order. Logical Methods in Computer Science, 12(2), 2016. URL: http://dx.doi.org/10.2168/LMCS-12(2:8)2016.
  8. Bogdan S. Chlebus. Domino-tiling games. J. Comput. Syst. Sci., 32(3):374-392, 1986. URL: http://dx.doi.org/10.1016/0022-0000(86)90036-X.
  9. Kousha Etessami, Moshe Y. Vardi, and Thomas Wilke. First-order logic with two variables and unary temporal logic. Inf. Comput., 179(2):279-295, 2002. URL: http://dx.doi.org/10.1006/inco.2001.2953.
  10. Erich Grädel, Martin Otto, and Eric Rosen. Two-variable logic with counting is decidable. In Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997, pages 306-317. IEEE Computer Society, 1997. URL: http://dx.doi.org/10.1109/LICS.1997.614957.
  11. Frederik Harwath and Nicole Schweikardt. On the locality of arb-invariant first-order formulas with modulo counting quantifiers. Logical Methods in Computer Science, 12(4), 2016. URL: http://dx.doi.org/10.2168/LMCS-12(4:8)2016.
  12. Lucas Heimberg, Dietrich Kuske, and Nicole Schweikardt. Hanf normal form for first-order logic with unary counting quantifiers. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 277-286. ACM, 2016. URL: http://dx.doi.org/10.1145/2933575.2934571.
  13. Emanuel Kieronski. On the complexity of the two-variable guarded fragment with transitive guards. Inf. Comput., 204(11):1663-1703, 2006. URL: http://dx.doi.org/10.1016/j.ic.2006.08.001.
  14. Andreas Krebs and A. V. Sreejith. Non-definability of languages by generalized first-order formulas over (n, +). In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012, pages 451-460. IEEE Computer Society, 2012. URL: http://dx.doi.org/10.1109/LICS.2012.55.
  15. Kamal Lodaya and A. V. Sreejith. Two-variable first order logic with counting quantifiers: Complexity results. In Émilie Charlier, Julien Leroy, and Michel Rigo, editors, Developments in Language Theory - 21st International Conference, DLT 2017, Liège, Belgium, August 7-11, 2017, Proceedings, volume 10396 of Lecture Notes in Computer Science, pages 260-271. Springer, 2017. URL: http://dx.doi.org/10.1007/978-3-319-62809-7_19.
  16. Maarten Marx and Maarten de Rijke. Semantic characterization of navigational XPath. In First Twente Data Management Workshop (TDM 2004) on XML Databases and Information Retrieval, pages 73-79, 2004. Google Scholar
  17. Juha Nurmonen. Counting modulo quantifiers on finite structures. Inf. Comput., 160(1-2):62-87, 2000. URL: http://dx.doi.org/10.1006/inco.1999.2842.
  18. Andreas Potthoff. Modulo-counting quantifiers over finite trees. Theor. Comput. Sci., 126(1):97-112, 1994. URL: http://dx.doi.org/10.1016/0304-3975(94)90270-4.
  19. Amitabha Roy and Howard Straubing. Definability of languages by generalized first-order formulas over n^+. SIAM J. Comput., 37(2):502-521, 2007. URL: http://dx.doi.org/10.1137/060658035.
  20. Dana Scott. A decision method for validity of sentences in two variables. Journal of Symbolic Logic, 27:477, 1962. Google Scholar
  21. A. V. Sreejith. Expressive completeness for LTL with modulo counting and group quantifiers. Electr. Notes Theor. Comput. Sci., 278:201-214, 2011. URL: http://dx.doi.org/10.1016/j.entcs.2011.10.016.
  22. Howard Straubing and Denis Thérien. Modular quantifiers. In Jörg Flum, Erich Grädel, and Thomas Wilke, editors, Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas]., volume 2 of Texts in Logic and Games, pages 613-628. Amsterdam University Press, 2008. Google Scholar
  23. Howard Straubing, Denis Thérien, and Wolfgang Thomas. Regular languages defined with generalized quanifiers. Inf. Comput., 118(2):289-301, 1995. URL: http://dx.doi.org/10.1006/inco.1995.1067.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact