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.