Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures
Aus International Center for Computational Logic
Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures
Luisa HerrmannLuisa Herrmann, Vincent PethVincent Peth, Sebastian RudolphSebastian Rudolph
Luisa Herrmann, Vincent Peth, Sebastian Rudolph
Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures
In Aniello Murano, Alexandra Silva, eds., CSL '24: Proceedings of the 32nd EACSL Annual Conference on Computer Science Logic 2024, volume 288 of LIPIcs, 33:1-33:19, 2024. Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures
In Aniello Murano, Alexandra Silva, eds., CSL '24: Proceedings of the 32nd EACSL Annual Conference on Computer Science Logic 2024, volume 288 of LIPIcs, 33:1-33:19, 2024. Schloss Dagstuhl - Leibniz-Zentrum für Informatik
- KurzfassungAbstract
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. - Weitere Informationen unter:Further Information: Link
- Projekt:Project: DeciGUT, ScaDS.AI
- Forschungsgruppe:Research Group: Computational LogicComputational Logic
@inproceedings{HPR2024,
author = {Luisa Herrmann and Vincent Peth and Sebastian Rudolph},
title = {Decidable (Ac)counting with Parikh and Muller: Adding Presburger
Arithmetic to Monadic Second-Order Logic over Tree-Interpretable
Structures},
editor = {Aniello Murano and Alexandra Silva},
booktitle = {CSL '24: Proceedings of the 32nd {EACSL} Annual Conference on
Computer Science Logic 2024},
series = {LIPIcs},
volume = {288},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2024},
pages = {33:1-33:19},
doi = {10.4230/LIPIcs.CSL.2024.33}
}