Computing measures of weak-MSO definable sets of trees

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.