Document Open Access Logo

Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures

Authors Luisa Herrmann , Vincent Peth , Sebastian Rudolph

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2024.33.pdf
  • Filesize: 1.04 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Theory of computation → Tree languages
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Automated reasoning
Keywords
  • MSO
  • BAPA
  • Parikh-Muller tree automata
  • decidability
  • MSO-interpretations

Metrics

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

Abstract

We propose ωMSO⋈BAPA , an expressive logic for describing countable structures, which subsumes and transcends both Counting Monadic Second-Order Logic (CMSO) and Boolean Algebra with Presburger Arithmetic (BAPA). We show that satisfiability of ωMSO⋈BAPA is decidable over the class of labeled infinite binary trees, whereas it becomes undecidable even for a rather mild relaxations. The decidability result is established by an elaborate multi-step transformation into a particular normal form, followed by the deployment of Parikh-Muller Tree Automata, a novel kind of automaton for infinite labeled binary trees, integrating and generalizing both Muller and Parikh automata while still exhibiting a decidable (in fact PSpace-complete) emptiness problem. By means of MSO-interpretations, we lift the decidability result to all tree-interpretable classes of structures, including the classes of finite/countable structures of bounded treewidth/cliquewidth/partitionwidth. We generalize the result further by showing that decidability is even preserved when coupling width-restricted ωMSO⋈BAPA with width-unrestricted two-variable logic with advanced counting. A final showcase demonstrates how our results can be leveraged to harvest decidability results for expressive μ-calculi extended by global Presburger constraints.

Cite As Get BibTex

Luisa Herrmann, Vincent Peth, and Sebastian Rudolph. Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 33:1-33:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.CSL.2024.33

Author Details

Luisa Herrmann
  • Computational Logic Group, TU Dresden, Germany
  • Center for Scalable Data Analytics and Artificial Intelligence Dresden/Leipzig, Germany
Vincent Peth
  • Département d’informatique de l’ÉNS, École normale supérieure, CNRS, PSL University, Paris, France
Sebastian Rudolph
  • Computational Logic Group, TU Dresden, Germany
  • Center for Scalable Data Analytics and Artificial Intelligence Dresden/Leipzig, Germany

Funding

BMBF (SCADS22B) and SMWK by funding ScaDS.AI Dresden/Leipzig.
  • Rudolph, Sebastian: European Research Council, Consolidator Grant DeciGUT (771779).

References

  1. Stefan Arnborg, Jens Lagergren, and Detlef Seese. Problems easy for tree-decomposable graphs (extended abstract). In Timo Lepistö and Arto Salomaa, editors, 15th International Colloquium on Automata, Languages and Programming (ICALP 1988), volume 317 of LNCS, pages 38-51. Springer, 1988. URL: https://doi.org/10.1007/3-540-19488-6_105.
  2. Franz Baader, Bartosz Bednarczyk, and Sebastian Rudolph. Satisfiability and query answering in description logics with global and local cardinality constraints. In Giuseppe De Giacomo, Alejandro Catalá, Bistra Dilkina, Michela Milano, Senén Barro, Alberto Bugarín, and Jérôme Lang, editors, 24th European Conference on Artificial Intelligence, (ECAI 2020) - Including 10th Conference on Prestigious Applications of Artificial Intelligence (PAIS 2020), volume 325 of Frontiers in Artificial Intelligence and Applications, pages 616-623. IOS Press, 2020. URL: https://doi.org/10.3233/FAIA200146.
  3. Franz Baader, Martin Buchheit, and Bernhard Hollunder. Cardinality restrictions on concepts. Artif. Intell., 88(1-2):195-213, 1996. URL: https://doi.org/10.1016/S0004-3702(96)00010-0.
  4. Franz Baader, Ian Horrocks, Carsten Lutz, and Uli Sattler. An Introduction to Description Logic. Cambridge University Press, 2017. URL: https://doi.org/10.1017/9781139025355.
  5. Bartosz Bednarczyk, Maja Orlowska, Anna Pacanowska, and Tony Tan. On classical decidable logics extended with percentage quantifiers and arithmetics. In Mikolaj Bojanczyk and Chandra Chekuri, editors, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021), volume 213 of LIPIcs, pages 36:1-36:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2021.36.
  6. Bartosz Bednarczyk and Sebastian Rudolph. Worst-case optimal querying of very expressive description logics with path expressions and succinct counting. In Sarit Kraus, editor, 28st International Joint Conference on Artificial Intelligence (IJCAI 2019), pages 1530-1536. ijcai.org, 2019. URL: https://doi.org/10.24963/ijcai.2019/212.
  7. Michael Benedikt, Egor V. Kostylev, and Tony Tan. Two variable logic with ultimately periodic counting. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020), volume 168 of LIPIcs, pages 112:1-112:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.ICALP.2020.112.
  8. Patrick Blackburn, Maarten de Rijke, and Yde Venema. Modal Logic, volume 53 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001. URL: https://doi.org/10.1017/CBO9781107050884.
  9. Patrick Blackburn, Johan F.A.K. van Benthem, and Frank Wolter, editors. Handbook of Modal Logic, volume 3 of Studies in logic and practical reasoning. North-Holland, 2007. Google Scholar
  10. Achim Blumensath. Structures of bounded partition width. PhD thesis, RWTH Aachen University, Germany, 2003. URL: http://sylvester.bth.rwth-aachen.de/dissertationen/2003/256/index.htm.
  11. Achim Blumensath. A model-theoretic characterisation of clique width. Annals of Pure and Applied Logic, 142(1-3):321-350, 2006. URL: https://doi.org/10.1016/j.apal.2006.02.004.
  12. Piero A. Bonatti, Carsten Lutz, Aniello Murano, and Moshe Y. Vardi. The complexity of enriched mu-calculi. Log. Methods Comput. Sci., 4(3), 2008. URL: https://doi.org/10.2168/LMCS-4(3:11)2008.
  13. Piero A. Bonatti and Adriano Peron. On the undecidability of logics with converse, nominals, recursion and counting. Artif. Intell., 158(1):75-96, 2004. URL: https://doi.org/10.1016/j.artint.2004.04.012.
  14. Diego Calvanese and Giuseppe De Giacomo. Expressive Description Logics, pages 193-236. Cambridge University Press, 2 edition, 2007. URL: https://doi.org/10.1017/CBO9780511711787.007.
  15. Diego Calvanese, Thomas Eiter, and Magdalena Ortiz. Answering regular path queries in expressive description logics: An automata-theoretic approach. In 22nd Conference on Artificial Intelligence (AAAI 2007), pages 391-396. AAAI Press, 2007. URL: http://www.aaai.org/Library/AAAI/2007/aaai07-061.php.
  16. Diego Calvanese, Thomas Eiter, and Magdalena Ortiz. Regular path queries in expressive description logics with nominals. In Craig Boutilier, editor, 21st International Joint Conference on Artificial Intelligence (IJCAI 2009), pages 714-720, 2009. URL: http://ijcai.org/Proceedings/09/Papers/124.pdf.
  17. Bruno Courcelle. The monadic second-order logic of graphs, II: Infinite graphs of bounded width. Mathematical Systems Theory, 21(1):187-221, 1988. URL: https://doi.org/10.1007/BF02088013.
  18. Bruno Courcelle. The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. Information and Computation, 85(1):12-75, 1990. URL: https://doi.org/10.1016/0890-5401(90)90043-H.
  19. Bruno Courcelle. The monadic second-order logic of graphs V. On closing the gap between definability and recognizability. Theoretical Computer Science, 80(2):153-202, 1991. URL: https://doi.org/10.1016/0304-3975(91)90387-H.
  20. Bruno Courcelle. Monadic second-order definable graph transductions: A survey. Theoretical Computer Science, 126(1):53-75, 1994. URL: https://doi.org/10.1016/0304-3975(94)90268-2.
  21. Bruno Courcelle. Clique-width of countable graphs: A compactness property. Discrete Mathematics, 276(1-3):127-148, 2004. URL: https://doi.org/10.1016/S0012-365X(03)00303-0.
  22. Bruno Courcelle and Joost Engelfriet. Graph Structure and Monadic Second-Order Logic - A Language-Theoretic Approach, volume 138 of Encyclopedia of mathematics and its applications. Cambridge University Press, 2012. URL: https://doi.org/10.1017/CBO9780511977619.
  23. Stéphane Demri and Denis Lugiez. Complexity of modal logics with presburger constraints. J. Appl. Log., 8(3):233-252, 2010. URL: https://doi.org/10.1016/j.jal.2010.03.001.
  24. E. Allen Emerson and Joseph Y. Halpern. "sometimes" and "not never" revisited: On branching versus linear time. In John R. Wright, Larry Landweber, Alan J. Demers, and Tim Teitelbaum, editors, 10th Annual ACM Symposium on Principles of Programming Languages (POPL 1983), pages 127-140. ACM Press, 1983. URL: https://doi.org/10.1145/567067.567081.
  25. Joost Engelfriet. A characterization of context-free NCE graph languages by monadic second-order logic on trees. In Hartmut Ehrig, Hans-Jörg Kreowski, and Grzegorz Rozenberg, editors, 4th International Workshop on Graph-Grammars and Their Application to Computer Science (Graph Grammars 1990), volume 532 of LNCS, pages 311-327. Springer, 1990. URL: https://doi.org/10.1007/BFb0017397.
  26. Thomas Feller, Tim S. Lyon, Piotr Ostropolski-Nalewaja, and Sebastian Rudolph. Decidability of querying first-order theories via countermodels of finite width, 2023. URL: https://arxiv.org/abs/2304.06348.
  27. Thomas Feller, Tim S. Lyon, Piotr Ostropolski-Nalewaja, and Sebastian Rudolph. Finite-cliquewidth sets of existential rules: Toward a general criterion for decidable yet highly expressive querying. In 26th International Conference on Database Theory (ICDT 2023), LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. Google Scholar
  28. Diego Figueira and Leonid Libkin. Path Logics for Querying Graphs: Combining Expressiveness and Efficiency. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2015), pages 329-340, 2015. URL: https://doi.org/10.1109/LICS.2015.39.
  29. Michael J. Fischer and Richard E. Ladner. Propositional dynamic logic of regular programs. J. Comput. Syst. Sci., 18(2):194-211, 1979. URL: https://doi.org/10.1016/0022-0000(79)90046-1.
  30. Seymour Ginsburg and Edwin H. Spanier. Bounded Algol-Like Languages. Transactions of the American Mathematical Society, 113(2):333, 1964. URL: https://doi.org/10.2307/1994067.
  31. Seymour Ginsburg and Edwin H. Spanier. Semigroups, Presburger formulas, and languages. Pacific Journal of Mathematics, 16(2):285-296, 1966. URL: https://doi.org/10.2140/pjm.1966.16.285.
  32. Erich Grädel, Martin Otto, and Eric Rosen. Two-variable logic with counting is decidable. In 12th Annual IEEE Symposium on Logic in Computer Science (LICS'97), pages 306-317. IEEE Computer Society, 1997. URL: https://doi.org/10.1109/LICS.1997.614957.
  33. Mario Grobler, Leif Sabellek, and Sebastian Siebertz. Parikh Automata on Infinite Words, 2023. URL: https://arxiv.org/abs/2301.08969.
  34. Mario Grobler, Leif Sabellek, and Sebastian Siebertz. Remarks on Parikh-recognizable omega-languages, 2023. URL: https://arxiv.org/abs/2307.07238.
  35. Mario Grobler and Sebastian Siebertz. Büchi-like characterizations for Parikh-recognizable omega-languages, 2023. URL: https://arxiv.org/abs/2302.04087.
  36. Martin Grohe and György Turán. Learnability and definability in trees and similar structures. Theory of Computing Systems, 37(1):193-220, 2004. URL: https://doi.org/10.1007/s00224-003-1112-8.
  37. Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann. Parikh automata over infinite words. In Anuj Dawar and Venkatesan Guruswami, editors, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022), volume 250 of LIPIcs, pages 40:1-40:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2022.40.
  38. Paul Hunter and Anuj Dawar. Complexity Bounds for Regular Games. In Joanna Jȩdrzejowicz and Andrzej Szepietowski, editors, Mathematical Foundations of Computer Science (MFCS 2005), LNCS, pages 495-506. Springer, 2005. URL: https://doi.org/10.1007/11549345_43.
  39. Felix Klaedtke. Automata-based decision procedures for weak arithmetics. PhD thesis, University of Freiburg, Freiburg im Breisgau, Germany, 2004. URL: http://freidok.ub.uni-freiburg.de/volltexte/1439/index.html.
  40. Felix Klaedtke and Harald Rueß. Parikh automata and monadic second-order logics with linear cardinality constraints. Technical Report 177, Albert-Ludwigs-Universität Freiburg, 2002. (revised version). Google Scholar
  41. Felix Klaedtke and Harald Rueß. Monadic second-order logics with cardinalities. In Jos C. M. Baeten, Jan Karel Lenstra, Joachim Parrow, and Gerhard J. Woeginger, editors, Automata, Languages and Programming, 30th International Colloquium (ICALP 2003), volume 2719 of LNCS, pages 681-696. Springer, 2003. URL: https://doi.org/10.1007/3-540-45061-0_54.
  42. Tomer Kotek, Helmut Veith, and Florian Zuleger. Monadic Second Order Finite Satisfiability and Unbounded Tree-Width. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), volume 62 of LIPIcs, pages 13:1-13:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.13.
  43. Dexter Kozen. Results on the propositional μ-calculus. In Mogens Nielsen and Erik Meineche Schmidt, editors, Automata, Languages and Programming, 9th Colloquium (ICALP 1982), volume 140 of LNCS, pages 348-359. Springer, 1982. URL: https://doi.org/10.1007/BFb0012782.
  44. Viktor Kuncak, Huu Hai Nguyen, and Martin Rinard. An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic. In David Hutchison, Takeo Kanade, Josef Kittler, Jon M. Kleinberg, Friedemann Mattern, John C. Mitchell, Moni Naor, Oscar Nierstrasz, C. Pandu Rangan, Bernhard Steffen, Madhu Sudan, Demetri Terzopoulos, Dough Tygar, Moshe Y. Vardi, Gerhard Weikum, and Robert Nieuwenhuis, editors, Automated Deduction (CADE 2005), volume 3632 of LNCS, pages 260-277. Springer, 2005. URL: https://doi.org/10.1007/11532231_20.
  45. Viktor Kuncak, Huu Hai Nguyen, and Martin Rinard. Deciding Boolean Algebra with Presburger Arithmetic. Journal of Automated Reasoning, 36(3):213-239, 2006. URL: https://doi.org/10.1007/s10817-006-9042-1.
  46. Aless Lasaruk and Thomas Sturm. Effective Quantifier Elimination for Presburger Arithmetic with Infinity. In Vladimir P. Gerdt, Ernst W. Mayr, and Evgenii V. Vorozhtsov, editors, Computer Algebra in Scientific Computing (CASC 2009), volume 5743 of LNCS, pages 195-212. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04103-7_18.
  47. Yensen Limón, Edgard Benítez-Guerrero, Everardo Bárcenas, Guillermo Molero-Castillo, and Alejandro Velázquez-Mena. A satisfiability algorithm for the mu-calculus for trees with presburger constraints. In 7th International Conference in Software Engineering Research and Innovation (CONISOFT 2019), pages 72-79, 2019. URL: https://doi.org/10.1109/CONISOFT.2019.00020.
  48. Yuri V. Matiyasevich. Hilbert’s Tenth Problem. Foundations of Computing. MIT Press, 1993. Google Scholar
  49. Rohit J. Parikh. On Context-Free Languages. Journal of the ACM, 13(4):570-581, 1966. URL: https://doi.org/10.1145/321356.321364.
  50. Michael O. Rabin. Decidability of Second-Order Theories and Automata on Infinite Trees. Transactions of the American Mathematical Society, 141:1-35, 1969. URL: https://doi.org/10.2307/1995086.
  51. Neil Robertson and P.D Seymour. Graph minors. III. Planar tree-width. Journal of Combinatorial Theory, Series B, 36(1):49-64, 1984. URL: https://doi.org/10.1016/0095-8956(84)90013-3.
  52. "Johann" Sebastian Rudolph. Presburger concept cardinality constraints in very expressive description logics - Allegro sexagenarioso ma non ritardando. In Carsten Lutz, Uli Sattler, Cesare Tinelli, Anni-Yasmin Turhan, and Frank Wolter, editors, Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, volume 11560 of LNCS, pages 542-561. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-22102-7_25.
  53. Sebastian Rudolph. Foundations of description logics. In Axel Polleres, Claudia d'Amato, Marcelo Arenas, Siegfried Handschuh, Paula Kroner, Sascha Ossowski, and Peter F. Patel-Schneider, editors, Lecture Notes of the 7th International Reasoning Web Summer School (RW'11), volume 6848 of LNCS, pages 76-136. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-23032-5_2.
  54. Stephan Tobies. The complexity of reasoning with cardinality restrictions and nominals in expressive description logics. J. Artif. Intell. Res., 12:199-217, 2000. URL: https://doi.org/10.1613/jair.705.
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