In this work we introduce new generalised quantifiers which allow us to express the Rabin-Mostowski index of automata. Our main results study expressive power and decidability of the monadic second-order (MSO) logic extended with these quantifiers. We study these problems in the realm of both $ω$-words and infinite trees. As it turns out, the pictures in these two cases are very different. In the case of $ω$-words the new quantifiers can be effectively expressed in pure MSO logic. In contrast, in the case of infinite trees, addition of these quantifiers leads to an undecidable formalism. To realise index-quantifier elimination, we consider the extension of MSO by game quantifiers. As a tool, we provide a specific quantifier-elimination procedure for them. Moreover, we introduce a novel construction of transducers realising strategies in $ω$-regular games with monadic parameters.

翻译：本文引入了一类新的广义量词，用以表达自动机的Rabin-Mostowski指数。我们的主要成果研究了在单子二阶逻辑（MSO）中扩展这些量词后的表达能力和可判定性。我们在$ω$-字和无限树两种领域中对这些问题进行了探讨。结果表明，这两种情况下的图景截然不同。在$ω$-字的情形中，新量词可在纯MSO逻辑中被有效地表达。相反，在无限树的情形中，添加这些量词会导致不可判定的形式系统。为实现指数量词的消去，我们考虑了通过博弈量词扩展的MSO逻辑。作为一种工具，我们为其提供了一种特定的量词消去过程。此外，我们引入了一种新颖的转换器构造方法，用于实现具有单子参数的$ω$-正则博弈中的策略。