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. 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 $\omega$MSO$\Join$BAPA.

翻译：我们提出$\omega$MSO$\Join$BAPA，一种用于描述可数结构的表达能力丰富的逻辑，它涵盖并超越了计数一元二阶逻辑(CMSO)和带有普雷斯伯格算术的布尔代数(BAPA)。我们证明，在标号无穷二叉树的类上，$\omega$MSO$\Join$BAPA的可满足性是可判定的。这一结果通过一个精细的多步变换转化为特定范式，随后应用帕里克-穆勒树自动机——一种用于标号无穷二叉树的新型自动机，它集成并推广了穆勒自动机和帕里克自动机，同时仍具有可判定的（实际上为PSpace完全的）空性问题。借助MSO解释，我们将可判定性结果提升到所有树可解释的结构类，包括有界树宽/团宽/划分宽的有限/可数结构类。我们注意到，即使对于$\omega$MSO$\Join$BAPA的一个相当温和的扩展，在（有限或无穷）标号树上的可满足性也会变得不可判定。