An axiom system of probabilistic Mu-calculus

Mu-calculus (a.k.a. μTL) is built up from modal/dynamic logic via adding the least fixpoint operator μ. This type of logic has attracted increasing attention since Kozen's seminal work. PμTL is a succinct probabilistic extension of the standard μTL obtained by making the modal operators probabilistic. Properties of this logic, such as expressiveness and satisfiability decision, have been studied elsewhere. We consider another important problem: the axiomatization of that logic. By extending the approaches of Kozen and Walukiewicz, we present an axiom system for PμTL. In addition, we show that the axiom system is complete for aconjunctive formulas.