We propose $\omega$MSO$\Join$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 $\omega$MSO$\Join$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 $\omega$MSO$\Join$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 $\mu$-calculi extended by global Presburger constraints.

翻译：我们提出$\omega$MSO$\Join$BAPA，一种描述可数结构的表达性逻辑，它包含并超越了计数单子二阶逻辑(CMSO)和Presburger算术的布尔代数(BAPA)。我们证明$\omega$MSO$\Join$BAPA在标记无穷二叉树类上的可满足性是可判定的，而即使对相当温和的松弛也会变得不可判定。该可判定性结果通过一个精心设计的多步变换到特定范式，随后引入Parikh-Muller树自动机（一种处理标记无穷二叉树的新型自动机，它集成并推广了Muller自动机和Parikh自动机，同时仍具有可判定的（实际上是PSpace完全的）空性判定问题）来建立。通过MSO解释，我们将可判定性结果提升到所有树可解释的结构类，包括有界树宽/团宽/划分宽的有限/可数结构类。我们进一步推广该结果，证明当将宽度受限的$\omega$MSO$\Join$BAPA与具有高级计数功能的宽度不受限的两变量逻辑耦合时，可判定性仍然保持。最后的示例展示了如何利用我们的结果为扩展了全局Presburger约束的表达性$\mu$演算导出可判定性结果。