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

ISBN: 978-3-95977-310-2
Download
Slides
DOI Link

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

Details
Bibtex

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}
}