On the Computability of Measures of Regular Sets of Infinite Trees

TL;DR

This paper extends the decidability results of the Rabin tree theorem to probabilistic settings, demonstrating how to compute the probability that a random infinite tree satisfies a given monadic second-order logic formula, and proving this probability is algebraic.

Contribution

It introduces a method to compute the probability of satisfaction for MSO logic over infinite trees and proves the algebraicity of this probability, advancing the understanding of probabilistic properties in infinite tree automata.

Findings

Probability is an algebraic number.

Provides an algorithm for probabilistic MSO satisfiability.

Extends classical results to probabilistic infinite trees.

Abstract

The Rabin tree theorem yields an algorithm to solve the satisfiability problem for monadic second-order logic over infinite trees. Here we solve the probabilistic variant of this problem. Namely, we show how to compute the probability that a randomly chosen tree satisfies a given formula. We additionally show that this probability is an algebraic number. This closes a line of research where similar results were shown for formalisms weaker than the full monadic second-order logic.