@article{Liu2022, 
author = {Wanwei Liu and Junnan Xu and David N. Jansen and Andrea Turrini and Lijun Zhang},
title = {An Axiom System of Probabilistic Mu-Calculus},
year = {2022},
journal = {Tsinghua Science and Technology},
volume = {27},
number = {2},
pages = {372-385},
keywords = {PμTL, axiom system, aconjunctive formula, tableau approach},
url = {https://www.sciopen.com/article/10.26599/TST.2020.9010054},
doi = {10.26599/TST.2020.9010054},
abstract = {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.}
}