You are not logged in |
Generalised Quantifiers Based on Rabin-Mostowski Index
- Speaker(s)
- Michał Skrzypczak
- Affiliation
- University of Warsaw
- Language of the talk
- English
- Date
- March 19, 2025, 2:15 p.m.
- Room
- room 5440
- Title in Polish
- Generalised Quantifiers Based on Rabin-Mostowski Index
- Seminar
- Seminar Automata Theory
I will present our novel results obtained with Denis Kuperberg, Damian Niwiński, and Paweł Parys. The framework is Monadic Second-Order (MSO) logic over \omega-words and infinite trees. We begin with the index problem, which asks, given a language, can it be recognised by an automaton of a given index. We want to view it as a property of languages and allow for nested expressions of this shape - more formally, we want to introduce quantifiers which express internally inside a formula when some property can be recognised by automata of a certain index. This leads to a formalism denoted MSO+I, an extension of MSO by Index Quantifiers.
We show two contrasting results:
- MSO+I effectively reduces to MSO over omega-words,
- MSO+I is undecidable over infinite trees.
To achieve the first result we study an intermediate concept, namely Game Quantifiers G (a concept dating back to Moschovakis) and prove that MSO+G reduces to MSO. Moreover, we show a novel construction of transducers realising involved strategies. This provides a direct way of showing how MSO+I reduces to MSO.
I will present our novel results obtained with Denis Kuperberg, Damian Niwiński, and Paweł Parys. The framework is Monadic Second-Order (MSO) logic over \omega-words and infinite trees. We begin with the index problem, which asks, given a language, can it be recognised by an automaton of a given index. We want to view it as a property of languages and allow for nested expressions of this shape - more formally, we want to introduce quantifiers which express internally inside a formula when some property can be recognised by automata of a certain index. This leads to a formalism denoted MSO+I, an extension of MSO by Index Quantifiers.
We show two contrasting results:
- MSO+I effectively reduces to MSO over omega-words,
- MSO+I is undecidable over infinite trees.
To achieve the first result we study an intermediate concept, namely Game Quantifiers G (a concept dating back to Moschovakis) and prove that MSO+G reduces to MSO. Moreover, we show a novel construction of transducers realising involved strategies. This provides a direct way of showing how MSO+I reduces to MSO.
