Abstract
The majority of existing probabilistic model checking case studies are based on well understood theoretical models and distributions. However, real-life probabilistic systems usually involve distribution parameters whose values are obtained by empirical measurements and thus are subject to small perturbations. In this paper, we consider perturbation analysis of reachability in the parametric models of these systems (i.e., parametric Markov chains) equipped with the norm of absolute distance. Our main contribution is a method to compute the asymptotic bounds in the form of condition numbers for constrained reachability probabilities against perturbations of the distribution parameters of the system. The adequacy of the method is demonstrated through experiments with the Zeroconf protocol and the hopping frog problem.
The work is supported by grant R-252-000-458-133 from Singapore Ministry of Education Academic Research Fund. The authors would like to thank Professor Mingsheng Ying for pointing them to perturbation theory and the anonymous referees for improving the draft of this paper.
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
Preview
Unable to display preview. Download preview PDF.
References
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)
Schweitzer, P.J.: Perturbation theory and finite Markov chains. Journal of Applied Probability 5(2), 401–413 (1968)
Cho, G.E., Meyer, C.D.: Comparison of perturbation bounds for the stationary distribution of a Markov chain. Linear Algebra Appl. 335, 137–150 (2000)
Solan, E., Vieille, N.: Perturbed Markov chains. J. Applied Prob., 107–122 (2003)
Heidergott, B.: Perturbation analysis of Markov chains. In: 9th International Workshop on Discrete Event Systems, WODES 2008, pp. 99–104 (2008)
Su, G., Rosenblum, D.S.: Asymptotic bounds for quantitative verification of perturbed probabilistic systems, proof details (2013), http://arxiv.org/abs/1304.7614
Konstantinov, M., Gu, D., Mehrmann, V., Petkov, P.: Perturbation Theory for Matrix Equations. Elsevier, Amsterdam (2003)
MATLAB: version 8.0 (R2012b). The MathWorks Inc., Natick, Massachusetts (2012)
Trefethen, L.N., Bau, D.: Numerical Linear Algebra. SIAM: Society for Industrial and Applied Mathematics (1997)
Daws, C.: Symbolic and parametric model checking of discrete-time markov chains. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 280–294. Springer, Heidelberg (2005)
Hahn, E., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. International Journal on Software Tools for Technology Transfer 13(1), 3–19 (2011)
Sen, K., Viswanathan, M., Agha, G.: Model-checking Markov chains in the presence of uncertainties. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 394–410. Springer, Heidelberg (2006)
Benedikt, M., Lenhardt, R., Worrell, J.: LTL model checking of interval Markov chains. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 32–46. Springer, Heidelberg (2013)
Alur, R., La Torre, S., Madhusudan, P.: Perturbed timed automata. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 70–85. Springer, Heidelberg (2005)
Bouyer, P., Markey, N., Reynier, P.-A.: Robust model-checking of linear-time properties in timed automata. In: Correa, J.R., Hevia, A., Kiwi, M. (eds.) LATIN 2006. LNCS, vol. 3887, pp. 238–249. Springer, Heidelberg (2006)
Cover, T.M., Thomas, J.A.: Elements of information theory. Wiley-Interscience, New York (1991)
Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Su, G., Rosenblum, D.S. (2013). Asymptotic Bounds for Quantitative Verification of Perturbed Probabilistic Systems. In: Groves, L., Sun, J. (eds) Formal Methods and Software Engineering. ICFEM 2013. Lecture Notes in Computer Science, vol 8144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-41202-8_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-41202-8_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-41201-1
Online ISBN: 978-3-642-41202-8
eBook Packages: Computer ScienceComputer Science (R0)