Abstract
The fundamentals of probabilistic model checking for Markovian models and temporal properties have been studied extensively in the past 20 years. Research on methods for computing conditional probabilities for temporal properties under temporal conditions is, however, comparably rare. For computing conditional probabilities or expected values under ω-regular conditions in Markov chains, we introduce a new transformation of Markov chains that incorporates the effect of the condition into the model. For Markov decision processes, we show that the task to compute maximal reachability probabilities under reachability conditions is solvable in polynomial time, while it was conjectured to be computationally hard. Using adaptions of known automata-based methods, our algorithm can be generalized for computing the maximal conditional probabilities for ω-regular events under ω-regular conditions. The feasibility of our algorithms is studied in two benchmark examples.
This work was in part funded by the DFG through the CRC 912 HAEC, the cluster of excellence cfAED, the project QuaOS, the DFG/NWO-project ROCKS, and by the ESF young researcher group IMData 100098198, and the EU-FP-7 grant 295261 (MEALS).
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Andrés, M.E., van Rossum, P.: Conditional probabilities over probabilistic and nondeterministic systems. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 157–172. Springer, Heidelberg (2008)
Andrés, M.E.: Quantitative Analysis of Information Leakage in Probabilistic and Nondeterministic Systems. PhD thesis, UB Nijmegen (2011)
Baier, C.: On the algorithmic verification of probabilistic systems. Universität Mannheim, Habilitation Thesis (1998)
Baier, C., Groesser, M., Ciesinski, F.: Quantitative analysis under fairness constraints. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 135–150. Springer, Heidelberg (2009)
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press (2008)
Baier, C., Klein, J., Klüppelholz, S., Märcker, S.: Computing conditional probabilities in Markovian models efficiently. Technical report, TU Dresden (2014), http://wwwtcs.inf.tu-dresden.de/ALGI/PUB/TACAS14/
Bianco, A., De Alfaro, L.: Model checking of probabilistic and non-deterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499–513. Springer, Heidelberg (1995)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (2000)
Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. Journal of the ACM 42(4), 857–907 (1995)
D’Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reachability analysis of probabilistic systems by successive refinements. In: de Alfaro, L., Gilmore, S. (eds.) PAPM-PROBMIV 2001. LNCS, vol. 2165, pp. 39–56. Springer, Heidelberg (2001)
de Alfaro, L.: Formal Verification of Probabilistic Systems. PhD thesis, Stanford University, Department of Computer Science (1997)
de Alfaro, L.: Computing minimum and maximum reachability times in probabilistic systems. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 66–81. Springer, Heidelberg (1999)
Gao, Y., Xu, M., Zhan, N., Zhang, L.: Model checking conditional CSL for continuous-time Markov chains. Information Processing Letters 113(1-2), 44–50 (2013)
Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6, 512–535 (1994)
Haverkort, B.: Performance of Computer Communication Systems: A Model-Based Approach. Wiley (1998)
Ji, M., Wu, D., Chen, Z.: Verification method of conditional probability based on automaton. Journal of Networks 8(6), 1329–1335 (2013)
Katoen, J.-P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Performance Evaluation 68(2), 90–104 (2011)
Kulkarni, V.: Modeling and Analysis of Stochastic Systems. Chapman & Hall (1995)
Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: A hybrid approach. STTT 6(2), 128–142 (2004)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)
Kwiatkowska, M., Norman, G., Parker, D.: The PRISM benchmark suite. In: QEST 2012. IEEE (2012)
Kwiatkowska, M., Norman, G., Sproston, J.: Probabilistic model checking of the IEEE 802.11 wireless local area network protocol. In: Hermanns, H., Segala, R. (eds.) PAPM-PROBMIV 2002. LNCS, vol. 2399, pp. 169–187. Springer, Heidelberg (2002)
Puterman, M.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons, Inc., New York (1994)
Vardi, M.: Automatic verification of probabilistic concurrent finite-state programs. In: FOCS 1985, pp. 327–338. IEEE (1985)
Vardi, M.Y.: Probabilistic linear-time model checking: An overview of the automata-theoretic approach. In: Katoen, J.-P. (ed.) ARTS 1999. LNCS, vol. 1601, pp. 265–276. Springer, Heidelberg (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baier, C., Klein, J., Klüppelholz, S., Märcker, S. (2014). Computing Conditional Probabilities in Markovian Models Efficiently. In: Ábrahám, E., Havelund, K. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2014. Lecture Notes in Computer Science, vol 8413. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54862-8_43
Download citation
DOI: https://doi.org/10.1007/978-3-642-54862-8_43
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54861-1
Online ISBN: 978-3-642-54862-8
eBook Packages: Computer ScienceComputer Science (R0)