Tractable Probabilistic mu-Calculus That Expresses Probabilistic Temporal Logics

Authors Pablo Castro, Cecilia Kilmurray, Nir Piterman

Thumbnail PDF


  • Filesize: 0.67 MB
  • 13 pages

Document Identifiers

Author Details

Pablo Castro
Cecilia Kilmurray
Nir Piterman

Cite AsGet BibTex

Pablo Castro, Cecilia Kilmurray, and Nir Piterman. Tractable Probabilistic mu-Calculus That Expresses Probabilistic Temporal Logics. In 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 30, pp. 211-223, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


We revisit a recently introduced probabilistic \mu-calculus and study an expressive fragment of it. By using the probabilistic quantification as an atomic operation of the calculus we establish a connection between the calculus and obligation games. The calculus we consider is strong enough to encode well-known logics such as pctl and pctl^*. Its game semantics is very similar to the game semantics of the classical mu-calculus (using parity obligation games instead of parity games). This leads to an optimal complexity of NP\cap co-NP for its finite model checking procedure. Furthermore, we investigate a (relatively) well-behaved fragment of this calculus: an extension of pctl with fixed points. An important feature of this extended version of pctl is that its model checking is only exponential w.r.t. the alternation depth of fixed points, one of the main characteristics of Kozen's mu-calculus.
  • mu-calculus
  • probabilistic logics
  • model checking
  • game semantics


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2008. Google Scholar
  2. A. Bianco and L. de Alfaro. Model checking of probabalistic and nondeterministic systems. In 15th Conference on Foundations of Software Technology and Theoretical Computer Science, volume 1026 of Lecture Notes in Computer Science, pages 499-513. Springer, 1995. Google Scholar
  3. K. Chatterjee and N. Piterman. Obligation blackwell games and p-automata. Technical report, arXiv:1206.5174, 2012. Google Scholar
  4. F. Ciesinski and C. Baier. LiQuor: A tool for qualitative and quantitative linear time analysis of reactive systems. In QEST, pages 131-132. IEEE Computer Society, 2006. Google Scholar
  5. R. Cleaveland, S. Purushothaman Iyer, and M. Narasimha. Probabilistic temporal logics via the modal mu-calculus. Theor. Comput. Sci., 342(2-3):316-350, 2005. Google Scholar
  6. A. Condon. The complexity of stochastic games. Inf. Comput., 96(2):203-224, 1992. Google Scholar
  7. E.A. Emerson and C. Lei. Efficient model checking in fragments of the μ-calculus. In LICS. IEEE Computer Society, 1986. Google Scholar
  8. A. Hinton, M.Z. Kwiatkowska, G. Norman, and D. Parker. PRISM: a tool for automatic verification of probabilistic systems. In TACAS, volume 3920 of Lecture Notes in Computer Science. Springer-Verlag, 2006. Google Scholar
  9. M. Huth and M.Z. Kwiatkowska. Quantitative analysis and model checking. In 12th IEEE Symposium on Logic in Computer Science, pages 111-122. IEEE Computer Society, 1997. Google Scholar
  10. M. Huth, N. Piterman, and D. Wagner. p-automata: New foundations for discrete-time probabilistic verification. Performance Evaluation, 69(7-8):356-378, 2012. Google Scholar
  11. M. Jurdzinski. Deciding the winner in parity games is in UP ∩ co-UP. Inf. Process. Lett., 68(3):119-124, 1998. Google Scholar
  12. D. Kozen. Results on the propositional μ-calculus. In Automata, Languages and Programming, volume 140 of Lecture Notes in Computer Science. Springer Berlin Heidelberg, 1982. Google Scholar
  13. A. McIver and C. Morgan. Results on the quantitative μ-calculus qMμ. ACM Trans. Comput. Log., 8(1), 2007. Google Scholar
  14. M. Mio. Game Semantics for Probabilistic μ-Calculi. PhD thesis, University of Edinburgh, 2012. Google Scholar
  15. M. Mio and A. Simpson. Łukasiewicz μ-calculus. In FICS, 2013. Google Scholar
  16. K. Scheider. Verification of Reactive Systems: Formal Methods and Algorithms. Springer, 2004. Google Scholar
  17. U. Zwick and M. Paterson. The complexity of mean payoff games on graphs. Theor. Comput. Sci., 158(1&2):343-359, 1996. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail