Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Piotr Ostropolski-Nalewaja (Diskussion | Beiträge) (Die Seite wurde neu angelegt: „{{Veranstaltung |Titel EN=Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Str…“) |
Piotr Ostropolski-Nalewaja (Diskussion | Beiträge) Keine Bearbeitungszusammenfassung |
||
| Zeile 1: | Zeile 1: | ||
{{Veranstaltung | {{Veranstaltung | ||
|Titel EN=Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures | |Titel EN=Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures | ||
|Beschreibung EN= | |Beschreibung EN=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. | ||
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. | |||
The talk will take place in a hybrid fashion, physically in the APB room 3027, and online through the link: | The talk will take place in a hybrid fashion, physically in the APB room 3027, and online through the link: | ||
Version vom 17. Mai 2023, 14:09 Uhr
Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures
Vortrag von Luisa Herrmann
- Veranstaltungsort: APB room 3027
- Beginn: 25. Mai 2023 um 11:00
- Ende: 25. Mai 2023 um 12:00
- Event series: Research Seminar Logic and AI
- iCal
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.
The talk will take place in a hybrid fashion, physically in the APB room 3027, and online through the link: https://bbb.tu-dresden.de/b/pio-zwt-smp-aus
Best regards,
Piotr Ostropolski-Nalewaja
