On the Computability of Measures of Regular Sets of Infinite Trees

The Rabin tree theorem yields an algorithm for solving the satisfiability problem for monadic second order logic over infinite trees. Here we solve the probabilistic variant of that problem: computing the probability that a randomly chosen tree satisfies a given formula. Our approach builds on Rabin’s correspondence between logical formulae and finite automata over infinite trees. Given a parity tree automaton, we construct a formula in Tarski’s theory of the reals \ (R, 0, 1, +, *, \) that precisely defines the measure—under the coin-flipping distribution—of the tree language recognised by the automaton. As a consequence, the resulting measure is an algebraic number and Tarski’s decidability theorem applies. The size of the constructed formula is exponential in the size of the automaton, whether nondeterministic or alternating, which gives us elementary algorithms for finding a representation of the measure and for comparing the measure with a given rational number. We further show that the coin-flipping measure can be replaced by a broader class of measures generated by stochastic branching processes, by reducing this case to the original problem. Our proof relies on a fixed point characterisation of definable tree languages. However, classical μ -calculi are ill-suited for our purpose, since Boolean operations on sets do not translate well to the arithmetic operations applied to their measures. We therefore introduce a new formalism—the unary μ -calculus —which allows us to translate fixed point equations over the powerset lattice of infinite trees to equations over a probabilistic powerdomain, a suitable subspace of \ (Rⁿ \).