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

A talk by Luisa Herrmann:
May 25, 2023
11 a.m. – noon
TU Dresden, APB/3027 | BigBlueButton
Join us now: https://bbb.tu-dresden.de/b/pio-zwt-smp-aus
https://iccl.inf.tu-dresden.de/web/Decidable_(Ac)counting_with_Parikh_and_Muller:_Adding_Presburger_Arithmetic_to_Monadic_Second-Order_Logic_over_Tree-Interpretable_Structures

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. This 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 observe that satisfiability over (finite or infinite) labeled trees becomes undecidable even for a rather mild extension of ωMSO⋈BAPA.