Probabilistic MSO Logic

We introduce a probabilistic extension of MSO logic, by adding
a second order expected value operator to the logic. This operator
chooses a subset of positions according to a simple probability
distribution. We show equivalence results between this logic and
probabilistic automata over finite and infinite words and also over
finite ranked trees. Finally, we look at problems that arise for
infinite trees.