Equivalence of Probabilistic mu-Calculus and p-Automata

An important characteristic of Kozen’s µ-calculus is its strong connection with parity alternating tree automata. Here, we show that the probabilistic µ-calculus µ^p-calculus and p-automata (parity alternating Markov chain automata) have an equally strong connection. Namely, for every µ^p-calculus formula we can construct a p-automaton that accepts exactly those Markov chains that satisfy the formula. For every p-automaton we can construct a µ^p-calculus formula satisfied in exactly those Markov chains that are accepted by the automaton. The translation in one direction relies on a normal form of the calculus and in the other direction on the usage of vectorial µ^p-calculus. The proofs use the game semantics of µ^p-calculus and automata to show that our translations are correct.