Generalised Quantifiers Based on Rabin-Mostowski Index

TL;DR

This paper introduces new generalized quantifiers based on the Rabin-Mostowski index, exploring their expressive power and decidability in MSO logic over infinite structures, revealing contrasting results for words and trees.

Contribution

It defines new quantifiers for the Rabin-Mostowski index, analyzes their impact on MSO logic's expressiveness and decidability, and develops a quantifier-elimination procedure and transducer constructions.

Findings

Quantifiers are expressible in MSO over ω-words.

Addition of quantifiers leads to undecidability over infinite trees.

Provides a transducer construction for strategies in ω-regular games.

Abstract

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 $\omega$-words and infinite trees. As it turns out, the pictures in these two cases are very different. In the case of $\omega$-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 $\omega$-regular games with monadic parameters.