Advertisement

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)

Abstract

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.

Notes

Acknowledgement

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).

References

  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).  https://doi.org/10.1145/380752.380871
  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).  https://doi.org/10.1007/3-540-51803-7_22CrossRefzbMATHGoogle 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).  https://doi.org/10.1007/3-540-60692-0_70CrossRefzbMATHGoogle 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).  https://doi.org/10.1109/LICS.2008.21
  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).  https://doi.org/10.4230/LIPIcs.STACS.2015.211
  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).  https://doi.org/10.1145/2933575.2934526
  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).  https://doi.org/10.1016/j.tcs.2005.03.048MathSciNetCrossRefzbMATHGoogle 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).  https://doi.org/10.1007/978-3-662-49674-9_16CrossRefzbMATHGoogle 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).  https://doi.org/10.1109/SFCS.1991.185392
  13. 13.
    Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Asp. Comput. 6(5), 512–535 (1994).  https://doi.org/10.1007/BF01211866CrossRefzbMATHGoogle 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).  https://doi.org/10.1109/LICS.1997.614940
  15. 15.
    Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22(3), 328–350 (1981).  https://doi.org/10.1016/0022-0000(81)90036-2MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Kozen, D.: Results on the propositional \(\mu \)-calculus. Theor. Comput. Sci. 27(3), 333–354 (1983).  https://doi.org/10.1016/0304-3975(82)90125-6Google 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).  https://doi.org/10.4230/LIPIcs.FSTTCS.2016.25
  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). https://www.ijcai.org/Abstract/15/129
  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).  https://doi.org/10.1007/3-540-36078-6_20CrossRefGoogle Scholar
  20. 20.
    McIver, A., Morgan, C.: Results on the quantitative \(\mu \)-calculus \(qM\mu \). ACM Trans. Comput. Log. 8(1), 3 (2007).  https://doi.org/10.1145/1182613.1182616Google 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).  https://doi.org/10.1007/978-3-642-19805-2_20CrossRefGoogle 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).  https://doi.org/10.1016/0304-3975(95)00136-0Google 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).  https://doi.org/10.1109/SFCS.1981.4
  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).  https://doi.org/10.1016/0890-5401(89)90031-XMathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Tamura, K.: Completeness of Kozen’s axiomatization for the modal mu-calculus: A simple proof. CoRR abs/1408.3560 (2014). http://arxiv.org/abs/1408.3560
  27. 27.
    Walukiewicz, I.: Completeness of Kozen’s axiomatisation of the propositional \(\mu \)-calculus. Inf. Comput. 157(1–2), 142–182 (2000).  https://doi.org/10.1006/inco.1999.2836Google 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