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.Events All Events
Anas Shahab
June 8, 2023
Join us (hybrid event)
Sophie Adama, Martin Bogdan
June 21, 2023
Join us (local event)
September 11, 2023
September 25, 2023
Register now
October 26, 2023