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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
de Alfaro, L.: Formal verification of probabilistic systems. Ph.D. thesis, Stanford University (1997), Technical report STAN-CS-TR-98-1601
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
Baier, C.: On algorithmic verification methods for probabilistic systems. Habilitationsschrift, Universität Mannheim: Fakultät für Mathematik und Informatik (1998)
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)
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_22
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_70
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
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
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
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.048
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_16
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
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/BF01211866
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
Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22(3), 328–350 (1981). https://doi.org/10.1016/0022-0000(81)90036-2
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-6
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
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
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_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.1182616
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_20
Morgan, C., McIver, A.: A probabilistic temporal calculus based on expectations. In: Proceedings of Formal Methods Pacific. Citeseer (1997)
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-0
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
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-X
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
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.2836
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).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Xu, J., Liu, W., Jansen, D.N., Zhang, L. (2019). An Axiomatisation of the Probabilistic \(\mu \)-Calculus. In: Ait-Ameur, Y., Qin, S. (eds) Formal Methods and Software Engineering. ICFEM 2019. Lecture Notes in Computer Science(), vol 11852. Springer, Cham. https://doi.org/10.1007/978-3-030-32409-4_26
Download citation
DOI: https://doi.org/10.1007/978-3-030-32409-4_26
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-32408-7
Online ISBN: 978-3-030-32409-4
eBook Packages: Computer ScienceComputer Science (R0)