[LiuSWZ] A Simple Probabilistic Extension of Modal Mu-calculus Liu, W.; Song, L.; Wang, J. and Zhang, L. In International Joint Conference on Artificial Intelligence (IJCAI), pages 882-888, AAAI Press, 2015.
Downloads: pdf, bibURL: http://ijcai.org/papers15/Abstracts/IJCAI15-129.html Abstract. Probabilistic systems are an important theme in AI domain. As the specification language, PCTL is the most frequently used logic for reasoning about probabilistic properties. In this paper, we present a natural and succinct probabilistic extension of μ-calculus, another prominent logic in the concurrency theory. We study the relationship with PCTL. Surprisingly, the expressiveness is highly orthogonal with PCTL. The proposed logic captures some useful properties which cannot be expressed in PCTL. We investigate the model checking and satisfiability problem, and show that the model checking problem is in UP cap co-UP, and the satisfiability checking can be decided via reducing into solving parity games. This is in contrast to PCTL as well, whose satisfiability checking is still an open problem.