Equivalence of probabilistic μ-calculus and p-automata

Abstract

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.