%0 Journal Article %1 Herrmann2023-yu %A Herrmann, Luisa %A Peth, Vincent %A Rudolph, Sebastian %D 2023 %K Adding Arithmetic Logic Muller Parikh Presburger Yaff monadic second-Order structures tree-interpretable %T Decidable (ac)counting with Parikh and Muller: Adding Presburger Arithmetic to monadic second-Order Logic over tree-interpretable structures %X We propose $ømega$MSO$\Join$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 $ømega$MSO$\Join$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 $ømega$MSO$\Join$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 $\mu$-calculi extended by global Presburger constraints.

@article{Herrmann2023-yu, abstract = {We propose $\omega$MSO$\Join$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 $\omega$MSO$\Join$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 $\omega$MSO$\Join$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 $\mu$-calculi extended by global Presburger constraints.}, added-at = {2025-01-07T14:18:00.000+0100}, author = {Herrmann, Luisa and Peth, Vincent and Rudolph, Sebastian}, biburl = {https://puma.scadsai.uni-leipzig.de/bibtex/207e7c5e3b97894076ed0117216fce40c/scadsfct}, eprint = {2305.01962}, interhash = {6523025f5ef802395952941b04f57bcd}, intrahash = {07e7c5e3b97894076ed0117216fce40c}, keywords = {Adding Arithmetic Logic Muller Parikh Presburger Yaff monadic second-Order structures tree-interpretable}, primaryclass = {cs.LO}, timestamp = {2025-01-31T12:03:45.000+0100}, title = {Decidable (ac)counting with Parikh and Muller: Adding Presburger Arithmetic to monadic second-Order Logic over tree-interpretable structures}, year = 2023 }