Probabilistic Modal μ-Calculus with Independent Product

  • Matteo Mio
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6604)


The probabilistic modal μ-calculus pLμ (often called the quantitative μ-calculus) is a generalization of the standard modal μ-calculus designed for expressing properties of probabilistic labeled transition systems. The syntax of pLμ formulas coincides with that of the standard modal μ-calculus. Two equivalent semantics have been studied for pLμ, both assigning to each process-state p a value in [0,1] representing the probability that the property expressed by the formula will hold in p: a denotational semantics and a game semantics given by means of two player stochastic games. In this paper we extend the logic pLμ with a second conjunction called product, whose semantics interprets the two conjuncts as probabilistically independent events. This extension allows one to encode useful operators, such as the modalities with probability one and with non-zero probability. We provide two semantics for this extended logic: one denotational and one based on a new class of games which we call tree games. The main result is the equivalence of the two semantics. The proof is carried out in ZFC set theory extended with Martin’s Axiom at the first uncountable cardinal.


  1. 1.
    Bertrand, N., Genest, B., Gimbert, H.: Qualitative determinacy and decidability of stochastic games with signals. In: LICS 2009, IEEE Symposium on Logic in Computer Science, Los Angeles, USA (2009)Google Scholar
  2. 2.
    Blackwell, D.: Infinite Gδ games with imperfect information. Matematyki Applicationes Mathematicae, Hugo Steinhaus Jubilee Volume (1969)Google Scholar
  3. 3.
    Brázdil, T., Brozek, V., ín Kucera, A., Obdrzálek, J.: Qualitative reachability in stochastic BPA games. In: STACS, pp. 207–218 (2009)Google Scholar
  4. 4.
    Brázdil, T., Brozek, V., Forejt, V., Kucera, A.: Stochastic games with branching-time winning objectives. In: LICS, pp. 349–358 (2006)Google Scholar
  5. 5.
    de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. Journal of Computer and System Sciences 68, 374–397 (2004)MathSciNetCrossRefGoogle Scholar
  6. 6.
    Deng, Y., van Glabbeek, R.: Characterising probabilistic processes logically. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 278–293. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  7. 7.
    Fischer, D., Gradel, E., Kaiser, L.: Model checking games for the quantitative μ-calculus. In: Theory of Computing Systems. Springer, New York (2009)Google Scholar
  8. 8.
    Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6 (1994)CrossRefGoogle Scholar
  9. 9.
    Huth, M., Kwiatkowska, M.: Quantitative analysis and model checking. In: LICS 1997, Washington, DC, USA, p. 111. IEEE Computer Society, Los Alamitos (1997)Google Scholar
  10. 10.
    Kozen, D.: Results on the propositional mu-calculus. Theoretical Computer Science, 333–354 (1983)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Martin, D.A., Solovay, R.M.: Internal Cohen extensions. Ann. Math. Logic 2, 143–178 (1970)MathSciNetCrossRefGoogle Scholar
  12. 12.
    McIver, A., Morgan, C.: Results on the quantitative μ-calculus qMμ. ACM Trans. Comput. Logic 8(1), 3 (2007)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Mio, M.: The equivalence of denotational and game semantics for the probabilistic μ-calculus. In: 7th Workshop on Fixed Points in Computer Science (2010)Google Scholar
  14. 14.
    Morgan, C., McIver, A.: A probabilistic temporal calculus based on expectations. In: Groves, L., Reeves, S. (eds.) Proc. Formal Methods. Springer, Heidelberg (1997)Google Scholar
  15. 15.
    Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Laboratory for Computer Science, M.I.T. (1995)Google Scholar
  16. 16.
    Stirling, C.: Modal and temporal logics for processes. Springer, Heidelberg (2001)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Matteo Mio
    • 1
  1. 1.LFCS, School of InformaticsUniversity of EdinburghUK

Personalised recommendations