An Axiom System of Probabilistic Mu-Calculus

Mu-calculus (a.k.a. $\mu$TL) is built up from modal/dynamic logic via adding the least fixpoint operator $\mu$. This type of logic has attracted increasing attention since Kozen’s seminal work. P $\mu$TL is a succinct probabilistic extension of the standard $\mu$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 $\mu$TL. In addition, we show that the axiom system is complete for aconjunctive formulas.