An Axiomatisation of the Probabilistic \mu -Calculus.

The probabilistic \(\mu \)-calculus (P\(\mu \)TL) is a simple and succinct probabilistic extension of the propositional \(\mu \)-calculus, by extending the ‘next’-operator with a probabilistic quantifier. We extend the approach developed by Walukiewicz for propositional \(\mu \)-calculus and provide an axiomatisation of P\(\mu \)TL. Our main contributions are a sound axiom system for P\(\mu \)TL, and a proof of its completeness for aconjunctive formulae.