Conditional Probabilities over Probabilistic and Nondeterministic Systems

  • Miguel E. Andrés
  • Peter van Rossum
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4963)


This paper introduces the logic cpCTL, which extends the probabilistic temporal logic pCTL with conditional probability, allowing one to express that the probability that φ is true given that ψ is true is at least a. We interpret cpCTL over Markov Chain and Markov Decision Processes. While model checking cpCTL over Markov Chains can be done with existing techniques, those techniques do not carry over to Markov Decision Processes. We present a model checking algorithm for Markov Decision Processes. We also study the class of schedulers that suffice to find the maximum and minimum probability that φ is true given that ψ is true. Finally, we present the notion of counterexamples for cpCTL model checking and provide a method for counterexample generation.


Conditional Probability Model Check Markov Decision Process Strongly Connect Component Model Check Algorithm 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. [AL06]
    Aljazzar, H., Leue, S.: Extended directed search for probabilistic timed reachability. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 33–51. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  2. [And06]
    Andrés, M.E.: Derivation of counterexamples for quantitative model checking. Master’s thesis, National University of Córdoba (2006)Google Scholar
  3. [BA95]
    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)Google Scholar
  4. [Bel57]
    Bellman, R.E.: A Markovian decision process. J. Math. Mech. 6, 679–684 (1957)zbMATHMathSciNetGoogle Scholar
  5. [BP05]
    Bhargava, M., Palamidessi, C.: Probabilistic anonymity. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 171–185. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  6. [CGJ+00]
    Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  7. [Cha88]
    Chaum, D.: The dining cryptographers problem: Unconditional sender and recipient untraceability. Journal of Cryptology 1(1), 65–75 (1988)zbMATHCrossRefMathSciNetGoogle Scholar
  8. [CL05]
    Camenisch, J., Lysyanskaya, A.: A formal treatment of onion routing. In: Shoup, V. (ed.) CRYPTO 2005. LNCS, vol. 3621, pp. 169–187. Springer, Heidelberg (2005)Google Scholar
  9. [DY83]
    Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)zbMATHCrossRefMathSciNetGoogle Scholar
  10. [FOO92]
    Fujioka, A., Okamoto, T., Ohta, K.: A practical secret voting scheme for large scale elections. In: Zheng, Y., Seberry, J. (eds.) AUSCRYPT 1992. LNCS, vol. 718, pp. 244–251. Springer, Heidelberg (1993)Google Scholar
  11. [FV97]
    Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer, Heidelberg (1997)zbMATHGoogle Scholar
  12. [HJ89]
    Hansson, H., Jonsson, B.: A framework for reasoning about time and reliability. In: Proceedings of Real Time Systems Symposium, pp. 102–111. IEEE, Los Alamitos (1989)Google Scholar
  13. [HK07]
    Han, T., Katoen, J.-P.: Counterexamples in probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 60–75. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  14. [LBB+01]
    Larsen, K.G., Behrmann, G., Brinksma, E., Fehnker, A., Hune, T.S., Petterson, P., Romijn, J.: As cheap as possible: Efficient cost-optimal reachability for priced timed automata. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, Springer, Heidelberg (2001)Google Scholar
  15. [PZ93]
    Pnueli, A., Zuck, L.D.: Probabilistic verification. Information and Computation 103(1), 1–29 (1993)zbMATHCrossRefMathSciNetGoogle Scholar
  16. [SV04]
    Sokolova, A., de Vink, E.P.: Probabilistic automata: System types, parallel composition and comparison. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 1–43. Springer, Heidelberg (2004)Google Scholar
  17. [SL95]
    Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. Nordic Journal of Computing 2(2), 250–273 (1995)zbMATHMathSciNetGoogle Scholar
  18. [Var85]
    Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state systems. In: Proc. 26th IEEE Symp. Found. Comp. Sci, pp. 327–338 (1985)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Miguel E. Andrés
    • 1
  • Peter van Rossum
    • 1
  1. 1.Institute for Computing and Information SciencesRadboud University NijmegenThe Netherlands

Personalised recommendations