Nie jesteś zalogowany |
Generalised Quantifiers Based on Rabin-Mostowski Index
- Prelegent(ci)
- Michał Skrzypczak
- Afiliacja
- University of Warsaw
- Język referatu
- angielski
- Termin
- 19 marca 2025 14:15
- Pokój
- p. 5440
- Tytuł w języku polskim
- Generalised Quantifiers Based on Rabin-Mostowski Index
- Seminarium
- Seminarium „Teoria automatów”
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.
