Advertisement

Perturbation Analysis in Verification of Discrete-Time Markov Chains

  • Taolue Chen
  • Yuan Feng
  • David S. Rosenblum
  • Guoxin Su
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8704)

Abstract

Perturbation analysis in probabilistic verification addresses the robustness and sensitivity problem for verification of stochastic models against qualitative and quantitative properties. We identify two types of perturbation bounds, namely non-asymptotic bounds and asymptotic bounds. Non-asymptotic bounds are exact, pointwise bounds that quantify the upper and lower bounds of the verification result subject to a given perturbation of the model, whereas asymptotic bounds are closed-form bounds that approximate non-asymptotic bounds by assuming that the given perturbation is sufficiently small. We perform perturbation analysis in the setting of Discrete-time Markov Chains. We consider three basic matrix norms to capture the perturbation distance, and focus on the computational aspect. Our main contributions include algorithms and tight complexity bounds for calculating both non-asymptotic bounds and asymptotic bounds with respect to the three perturbation distances.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Allender, E., Bürgisser, P., Kjeldgaard-Pedersen, J., Miltersen, P.B.: On the complexity of numerical analysis. SIAM J. Comput. 38(5), 1987–2006 (2009)CrossRefzbMATHGoogle Scholar
  2. 2.
    Allender, E., Ogihara, M.: Relationships among PL, #L, and the determinant. ITA 30(1), 1–21 (1996)zbMATHMathSciNetGoogle Scholar
  3. 3.
    Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press (2008)Google Scholar
  4. 4.
    Bartocci, E., Grosu, R., Katsaros, P., Ramakrishnan, C.R., Smolka, S.A.: Model repair for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 326–340. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  5. 5.
    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)Google Scholar
  6. 6.
    Bianco, A., de Alfaro, L.: Model checking of probabalistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499–513. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  7. 7.
    Canny, J.F.: Some algebraic and geometric computations in PSPACE. In: Simon, J. (ed.) STOC, pp. 460–467. ACM (1988)Google Scholar
  8. 8.
    Chatterjee, K.: Robustness of structurally equivalent concurrent parity games. In: Birkedal, L. (ed.) FOSSACS 2012. LNCS, vol. 7213, pp. 270–285. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  9. 9.
    Chatterjee, K., Sen, K., Henzinger, T.A.: Model-checking ω-regular properties of Interval Markov Chains. In: Amadio, R. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 302–317. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  10. 10.
    Chen, T., Feng, Y., Rosenblum, D.S., Su, G.: Perturbation analysis in verification of discrete-time Markov chains. Technical report, Middlesex University London (2014), http://www.cs.mdx.ac.uk/staffpages/taoluechen/pub-papers/concur14-full.pdf
  11. 11.
    Chen, T., Hahn, E., Han, T., Kwiatkowska, M., Qu, H., Zhang, L.: Model repair for Markov decision processes. In: TASE 2013, pp. 85–92 (July 2013)Google Scholar
  12. 12.
    Chen, T., Han, T., Kwiatkowska, M.Z.: On the complexity of model checking interval-valued discrete time Markov chains. Inf. Process. Lett. 113(7), 210–216 (2013)CrossRefzbMATHMathSciNetGoogle Scholar
  13. 13.
    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)CrossRefMathSciNetGoogle Scholar
  14. 14.
    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)CrossRefGoogle Scholar
  15. 15.
    Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov processes. Theor. Comput. Sci. 318(3), 323–354 (2004)CrossRefzbMATHMathSciNetGoogle Scholar
  16. 16.
    Donaldson, R., Gilbert, D.: A model checking approach to the parameter estimation of biochemical pathways. In: Heiner, M., Uhrmacher, A.M. (eds.) CMSB 2008. LNCS (LNBI), vol. 5307, pp. 269–287. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  17. 17.
    Etessami, K., Yannakakis, M.: Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations. J. ACM 56(1) (2009)Google Scholar
  18. 18.
    Filieri, A., Ghezzi, C., Tamburrelli, G.: Run-time efficient probabilistic model checking. In: ICSE 2011, New York, NY, USA, pp. 341–350 (2011)Google Scholar
  19. 19.
    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)CrossRefGoogle Scholar
  20. 20.
    Hahn, E.M., Han, T., Zhang, L.: Synthesis for PCTL in parametric Markov decision processes. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 146–161. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  21. 21.
    Han, T., Katoen, J.-P., Mereacre, A.: Approximate parameter synthesis for probabilistic time-bounded reachability. In: RTSS, pp. 173–182. IEEE Computer Society (2008)Google Scholar
  22. 22.
    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)CrossRefGoogle Scholar
  23. 23.
    Murdock, J.A.: Perturbation: Theory and Method. John Wiley & Sons, Inc. (1991)Google Scholar
  24. 24.
    Puggelli, A., Li, W., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Polynomial-time verification of PCTL properties of MDPs with convex uncertainties. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 527–542. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  25. 25.
    Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, New York (1994)Google Scholar
  26. 26.
    Sahni, S.: Computationally related problems. SIAM Journal on Computing 3, 262–279 (1974)CrossRefMathSciNetGoogle Scholar
  27. 27.
    Schweitzer, P.J.: Perturbation theory and finite Markov chains. Journal of Applied Probability 5(2), 401–413 (1968)CrossRefzbMATHMathSciNetGoogle Scholar
  28. 28.
    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)CrossRefGoogle Scholar
  29. 29.
    Solan, E., Vieille, N.: Perturbed Markov chains. J. Applied Prob. 40(1), 107–122 (2003)CrossRefzbMATHMathSciNetGoogle Scholar
  30. 30.
    Su, G., Rosenblum, D.S.: Asymptotic bounds for quantitative verification of perturbed probabilistic systems. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol. 8144, pp. 297–312. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  31. 31.
    Su, G., Rosenblum, D.S.: Perturbation analysis of stochastic systems with empirical distribution parameters. In: ICSE, pp. 311–321. ACM (2014)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Taolue Chen
    • 1
  • Yuan Feng
    • 2
  • David S. Rosenblum
    • 3
  • Guoxin Su
    • 3
  1. 1.Department of Computer ScienceMiddlesex UniversityLondonUK
  2. 2.Centre for Quantum Computation and Intelligent SystemsUniversity of TechnologySydneyAustralia
  3. 3.Department of Computer Science, School of ComputingNational University of SingaporeSingapore

Personalised recommendations