An Axiomatisation of the Probabilistic \(\mu \)-Calculus

  • Junnan Xu
  • Wanwei Liu
  • David N. Jansen
  • Lijun ZhangEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11852)


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.



This work is supported by the National Natural Science Foundation of China (Grants Nos. 61761136011,61532019), and the Guangdong Science and Technology Department (Grant No. 2018B010107004).


  1. 1.
    de Alfaro, L.: Formal verification of probabilistic systems. Ph.D. thesis, Stanford University (1997), Technical report STAN-CS-TR-98-1601Google Scholar
  2. 2.
    de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. In: 33rd ACM Symposium on Theory of Computing, STOC 2001, pp. 675–683. ACM, New York (2001).
  3. 3.
    Baier, C.: On algorithmic verification methods for probabilistic systems. Habilitationsschrift, Universität Mannheim: Fakultät für Mathematik und Informatik (1998)Google Scholar
  4. 4.
    Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)zbMATHGoogle Scholar
  5. 5.
    Banieqbal, B., Barringer, H.: Temporal logic with fixed points. In: Banieqbal, B., Barringer, H., Pnueli, A. (eds.) Temporal Logic in Specification. LNCS, vol. 398, pp. 62–74. Springer, Heidelberg (1989). Scholar
  6. 6.
    Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499–513. Springer, Heidelberg (1995). Scholar
  7. 7.
    Brázdil, T., Forejt, V., Křetínský, J., Kučera, A.: The satisfiability problem for probabilistic CTL. In: Twenty-Third Annual IEEE Symposium on Logic in Computer Science, Los Alamitos, Calif, pp. 391–402. IEEE (2008).
  8. 8.
    Castro, P., Kilmurray, C., Piterman, N.: Tractable probabilistic \(\mu \)-calculus that expresses probabilistic temporal logics. In: Mayr, E.W., Ollinger, N. (eds.) 32nd International Symposium on Theoretical Aspects of Computer Science: STACS 2015. LIPIcs, vol. 30, pp. 211–223. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2015).
  9. 9.
    Chakraborty, S., Katoen, J.-P.: On the satisfiability of some simple probabilistic logics. In: ACM (ed.) LICS, New York, pp. 56–65 (2016).
  10. 10.
    Cleaveland, R., Iyer, S.P., Narasimha, M.: Probabilistic temporal logics via the modal mu-calculus. Theor. Comput. Sci. 342(2–3), 316–350 (2005). Scholar
  11. 11.
    Dimitrova, R., Ferrer Fioriti, L.M., Hermanns, H., Majumdar, R.: Probabilistic CTL\(^{*}\): the deductive way. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 280–296. Springer, Heidelberg (2016). Scholar
  12. 12.
    Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy (extended abstract). In: Proceedings 32nd Annual Symposium of Foundations of Computer Science: FOCS, pp. 368–377. IEEE (1991).
  13. 13.
    Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Asp. Comput. 6(5), 512–535 (1994). Scholar
  14. 14.
    Huth, M., Kwiatkowska, M.: Quantitative analysis and model checking. In: 12th Annual IEEE Symposium on Logic in Computer Science, Los Alamitos, Calif, pp. 111–122. IEEE (1997).
  15. 15.
    Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22(3), 328–350 (1981). Scholar
  16. 16.
    Kozen, D.: Results on the propositional \(\mu \)-calculus. Theor. Comput. Sci. 27(3), 333–354 (1983). Scholar
  17. 17.
    Larsen, K.G., Mardare, R., Xue, B.: Probabilistic mu-calculus: decidability and complete axiomatization. In: Lal, A., Akshay, S., Saurabh, S., Sen, S. (eds.) 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science: FSTTCS. LIPIcs, vol. 65, pp. 25:1–25:18. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2016).
  18. 18.
    Liu, W., Song, L., Wang, J., Zhang, L.: A simple probabilistic extension of modal mu-calculus. In: Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, Palo Alto, Calif, pp. 882–888. AAAI Press (2015).
  19. 19.
    McIver, A.K., Morgan, C.C.: Games, probability, and the quantitative \(\upmu \)-calculus \(qM\mu \). In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS (LNAI), vol. 2514, pp. 292–310. Springer, Heidelberg (2002). Scholar
  20. 20.
    McIver, A., Morgan, C.: Results on the quantitative \(\mu \)-calculus \(qM\mu \). ACM Trans. Comput. Log. 8(1), 3 (2007). Scholar
  21. 21.
    Mio, M.: Probabilistic modal \(\mu \)-calculus with independent product. In: Hofmann, M. (ed.) FoSSaCS 2011. LNCS, vol. 6604, pp. 290–304. Springer, Heidelberg (2011). Scholar
  22. 22.
    Morgan, C., McIver, A.: A probabilistic temporal calculus based on expectations. In: Proceedings of Formal Methods Pacific. Citeseer (1997)Google Scholar
  23. 23.
    Niwiński, D., Walukiewicz, I.: Games for the \({\mu }\)-calculus. Theor. Comput. Sci. 163(1–2), 99–116 (1996). Scholar
  24. 24.
    Pratt, V.R.: A decidable mu-calculus: Preliminary report. In: 22nd Annual Symposium on Foundations of Computer Science, Los Angeles, pp. 421–427. IEEE (1981).
  25. 25.
    Streett, R.S., Emerson, E.A.: An automata theoretic decision procedure for the propositional mu-calculus. Inf. Comput. 81(3), 249–264 (1989). Scholar
  26. 26.
    Tamura, K.: Completeness of Kozen’s axiomatization for the modal mu-calculus: A simple proof. CoRR abs/1408.3560 (2014).
  27. 27.
    Walukiewicz, I.: Completeness of Kozen’s axiomatisation of the propositional \(\mu \)-calculus. Inf. Comput. 157(1–2), 142–182 (2000). Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Junnan Xu
    • 1
    • 2
  • Wanwei Liu
    • 3
  • David N. Jansen
    • 1
    • 4
  • Lijun Zhang
    • 1
    • 2
    • 4
    Email author
  1. 1.Institute of Software, Chinese Academy of SciencesBeijingChina
  2. 2.University of Chinese Academy of SciencesBeijingChina
  3. 3.College of Computer ScienceNational University of Defense TechnologyChangshaChina
  4. 4.Institute of Intelligent SoftwareGuangzhouChina

Personalised recommendations