Computing measures of weak-MSO definable sets of trees
- Prelegent(ci)
- Michał Skrzypczak
- Afiliacja
- Uniwersytet Warszawski
- Termin
- 4 grudnia 2019 14:15
- Pokój
- p. 5050
- Seminarium
- Seminarium „Teoria automatów”
Michalewski and Mio posed a fundamental question about the possibility of computing standard measures of regular languages of infinite trees. A positive solution (i.e. an algorithm) would allow us to tackle quantitatively a variety of specification logics, like CTL* etc. Unfortunately, the general problem seems to be difficult: we only know that all these languages are measurable and some of them have irrational (but algebraic) measures.
During the talk I will present a recent advance showing how to compute measures of languages definable in weak Monadic Second-Order logic. Although the logic is not strong enough to capture path-quantifiers (like in CTL*); it is already fairly expressive, containing whole First-Order logic. Thus, the difficulties related to unrestricted alternation of quantifiers are fully present here.
The results were obtained in cooperation with Damian Niwiński and Marcin Przybyłko.