×

On abstraction of probabilistic systems. (English) Zbl 1426.68167

Remke, Anne (ed.) et al., Stochastic model checking. Rigorous dependability analysis using model checking techniques for stochastic systems. International autumn school, ROCKS 2012, Vahrn, Italy, October 22–26, 2012. Advanced lectures. Berlin: Springer. Lect. Notes Comput. Sci. 8453, 87-116 (2014).
Summary: Probabilistic model checking extends traditional model checking by incorporating quantitative information about the probability of system transitions. However, probabilistic models that describe interesting behavior are often too complex for straightforward analysis. Abstraction is one way to deal with this complexity: instead of analyzing the (“concrete”) model, a simpler (“abstract”) model that preserves the relevant properties is built and analyzed. This paper surveys various abstraction techniques proposed in the past decade. For each abstraction technique we identify in what sense properties are preserved or provide alternatively suitable boundaries.
For the entire collection see [Zbl 1298.68033].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] de Alfaro, L., Roy, P.: Magnifying-lens abstraction for Markov decision processes. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 325–338. Springer, Heidelberg (2007) · Zbl 1135.68486 · doi:10.1007/978-3-540-73368-3_38
[2] Aljazzar, H., Leue, S.: Directed explicit state-space search in the generation of counterexamples for stochastic model checking. IEEE Trans. Software Eng. 36(1), 37–60 (2010) · doi:10.1109/TSE.2009.57
[3] Aziz, A., Singhal, V., Balarin, F., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: It usually works: The temporal logic of stochastic systems. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 155–165. Springer, Heidelberg (1995) · doi:10.1007/3-540-60045-0_48
[4] Baier, C., Katoen, J.-P.: Principles of model checking. MIT Press, Cambridge (2008) · Zbl 1179.68076
[5] Baier, C., Katoen, J.-P., Hermanns, H., Wolf, V.: Comparative branching-time semantics for Markov chains. Information and Computation 200(2), 149–214 (2005) · Zbl 1101.68053 · doi:10.1016/j.ic.2005.03.001
[6] 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) · Zbl 1354.68167 · doi:10.1007/3-540-60692-0_70
[7] Bozzano, M., Cimatti, A., Katoen, J.-P., Nguyen, V.Y., Noll, T., Roveri, M.: Safety, dependability and performance analysis of extended aadl models. Comput. J. 54(5), 754–775 (2011) · doi:10.1093/comjnl/bxq024
[8] Chadha, R., Viswanathan, M.: A counterexample-guided abstraction-refinement framework for markov decision processes. ACM Trans. Comput. Log. 12(1), 1 (2010) · Zbl 1351.68154 · doi:10.1145/1838552.1838553
[9] Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: Prism-games: A model checker for stochastic multi-player games. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 185–191. Springer, Heidelberg (2013) · Zbl 1381.68151 · doi:10.1007/978-3-642-36742-7_13
[10] Clarke, E., 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) · Zbl 0974.68517 · doi:10.1007/10722167_15
[11] Condon, A.: The complexity of stochastic games. Information and Computation 96(2), 203–224 (1992) · Zbl 0756.90103 · doi:10.1016/0890-5401(92)90048-K
[12] D’Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reachability analysis of probabilistic systems by successive refinements. In: de Luca, L., Gilmore, S. (eds.) PAPM-PROBMIV 2001. LNCS, vol. 2165, pp. 39–56. Springer, Heidelberg (2001) · Zbl 1007.68131 · doi:10.1007/3-540-44804-7_3
[13] D’Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reduction and refinement strategies for probabilistic analysis. In: Hermanns, H., Segala, R. (eds.) PAPM-PROBMIV 2002. LNCS, vol. 2399, pp. 57–76. Springer, Heidelberg (2002) · Zbl 1065.68582 · doi:10.1007/3-540-45605-8_5
[14] Dehnert, C., Katoen, J.-P., Parker, D.: SMT-based bisimulation minimisation of markov models. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 28–47. Springer, Heidelberg (2013) · Zbl 1426.68168 · doi:10.1007/978-3-642-35873-9_5
[15] Delahaye, B., Katoen, J.-P., Larsen, K.G., Legay, A., Pedersen, M.L., Sher, F., Wąsowski, A.: Abstract probabilistic automata. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 324–339. Springer, Heidelberg (2011) · Zbl 1317.68095 · doi:10.1007/978-3-642-18275-4_23
[16] Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Approximating labelled Markov processes. Information and Computation 184(1), 160–200 (2003) · Zbl 1028.68091 · doi:10.1016/S0890-5401(03)00051-8
[17] Donaldson, A.F., Miller, A.: Symmetry reduction for probabilistic model checking using generic representatives. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 9–23. Springer, Heidelberg (2006) · Zbl 1161.68564 · doi:10.1007/11901914_4
[18] Eisentraut, C., Hermanns, H., Schuster, J., Turrini, A., Zhang, L.: The quest for minimal quotients for probabilistic automata. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 16–31. Springer, Heidelberg (2013) · Zbl 1381.68115 · doi:10.1007/978-3-642-36742-7_2
[19] Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming 2(3), 241–266 (1982) · Zbl 0514.68032 · doi:10.1016/0167-6423(83)90017-5
[20] Fecher, H., Leucker, M., Wolf, V.: Don’t know in probabilistic systems. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 71–88. Springer, Heidelberg (2006) · Zbl 1178.68341 · doi:10.1007/11691617_5
[21] Feng, L., Kwiatkowska, M.Z., Parker, D.: Compositional verification of probabilistic systems using learning. In: QEST, pp. 133–142. IEEE Computer Society (2010) · doi:10.1109/QEST.2010.24
[22] Ferrer Fioriti, L.M., Hahn, E.M., Hermanns, H., Wachter, B.: Variable probabilistic abstraction refinement. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 300–316. Springer, Heidelberg (2012) · Zbl 1374.68347 · doi:10.1007/978-3-642-33386-6_24
[23] Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: Pass: Abstraction refinement for infinite probabilistic models. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 353–357. Springer, Heidelberg (2010) · Zbl 05702255 · doi:10.1007/978-3-642-12002-2_30
[24] Han, T., Katoen, J.-P.: Counterexamples in probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 72–86. Springer, Heidelberg (2007) · Zbl 1186.68293 · doi:10.1007/978-3-540-71209-1_8
[25] Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6(5), 512–535 (1994) · Zbl 0820.68113 · doi:10.1007/BF01211866
[26] Henzinger, T.A., Mateescu, M., Wolf, V.: Sliding window abstraction for infinite Markov chains. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 337–352. Springer, Heidelberg (2009) · Zbl 1242.60079 · doi:10.1007/978-3-642-02658-4_27
[27] Hermanns, H., Wachter, B., Zhang, L.: Probabilistic CEGAR. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 162–175. Springer, Heidelberg (2008) · Zbl 1155.68438 · doi:10.1007/978-3-540-70545-1_16
[28] Huth, M., Jagadeesan, R., Schmidt, D.: Modal transition systems: A foundation for three-valued program analysis. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 155–169. Springer, Heidelberg (2001) · Zbl 0987.68849 · doi:10.1007/3-540-45309-1_11
[29] Jansen, D.N., Song, L., Zhang, L.: Revisiting weak simulation for substochastic Markov chains. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 209–224. Springer, Heidelberg (2013) · Zbl 06294369 · doi:10.1007/978-3-642-40196-1_18
[30] Jansen, N., Ábrahám, E., Katelaan, J., Wimmer, R., Katoen, J.-P., Becker, B.: Hierarchical counterexamples for discrete-time markov chains. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 443–452. Springer, Heidelberg (2011) · Zbl 1348.68139 · doi:10.1007/978-3-642-24372-1_33
[31] Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: Proc. LICS 1991, pp. 266–277. IEEE Comp. Soc. Pr. (1991) · doi:10.1109/LICS.1991.151651
[32] Katoen, J.-P., Kemna, T., Zapreev, I., Jansen, D.N.: Bisimulation minimisation mostly speeds up probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 87–101. Springer, Heidelberg (2007) · Zbl 1186.68296 · doi:10.1007/978-3-540-71209-1_9
[33] Katoen, J.-P., Klink, D., Leucker, M., Wolf, V.: Three-valued abstraction for probabilistic systems. JLAP 81(4), 356–389 (2012) · Zbl 1277.68219
[34] Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: A game-based abstraction-refinement framework for markov decision processes. Formal Methods in System Design 36(3), 246–280 (2010) · Zbl 1233.90276 · doi:10.1007/s10703-010-0097-6
[35] Kattenbelt, M., Kwiatkowska, M.Z., Norman, G., Parker, D.: A game-based abstraction-refinement framework for markov decision processes. Formal Methods in System Design 36(3), 246–280 (2010) · Zbl 1233.90276 · doi:10.1007/s10703-010-0097-6
[36] Komuravelli, A., Păsăreanu, C.S., Clarke, E.M.: Assume-guarantee abstraction refinement for probabilistic systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 310–326. Springer, Heidelberg (2012) · Zbl 06070753 · doi:10.1007/978-3-642-31424-7_25
[37] Kwiatkowska, M., Norman, G., Parker, D.: Symmetry reduction for probabilistic model checking. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 234–248. Springer, Heidelberg (2006) · Zbl 1188.68194 · doi:10.1007/11817963_23
[38] 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) · Zbl 05940745 · doi:10.1007/978-3-642-22110-1_47
[39] Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Assume-guarantee verification for probabilistic systems. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 23–37. Springer, Heidelberg (2010) · Zbl 1284.68406 · doi:10.1007/978-3-642-12002-2_3
[40] Larsen, K.G., Thomsen, B.: A modal process logic. In: Proc. LICS 1988, pp. 203–210. Los Alamitos, Calif (1988)
[41] Larsen, K.G., Thomsen, B.: A modal process logic. In: LICS, pp. 203–210 (1988) · doi:10.1109/LICS.1988.5119
[42] McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006) · Zbl 1188.68196 · doi:10.1007/11817963_14
[43] Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. Nordic Journal of Computing 2, 250–273 (1995) · Zbl 0839.68067
[44] Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: FOCS, pp. 327–338. IEEE Comp. Soc. Pr., Washington, DC (1985) · doi:10.1109/SFCS.1985.12
[45] Wachter, B.: Refined probabilistic abstraction. Ph.D. thesis, Universität des Saarlandes, Saarbrücken (2011)
[46] Wachter, B., Zhang, L.: Best probabilistic transformers. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 362–379. Springer, Heidelberg (2010) · Zbl 1273.68244 · doi:10.1007/978-3-642-11319-2_26
[47] Wimmer, R., Herbstritt, M., Hermanns, H., Strampp, K., Becker, B.: Sigref- a symbolic bisimulation tool box. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 477–492. Springer, Heidelberg (2006) · Zbl 1161.68631 · doi:10.1007/11901914_35
[48] Wimmer, R., Jansen, N., Ábrahám, E., Becker, B., Katoen, J.-P.: Minimal critical subsystems for discrete-time markov models. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 299–314. Springer, Heidelberg (2012) · Zbl 1352.68167 · doi:10.1007/978-3-642-28756-5_21
[49] Wimmer, R., Jansen, N., Vorpahl, A., Ábrahám, E., Katoen, J.-P., Becker, B.: High-level counterexamples for probabilistic automata. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 39–54. Springer, Heidelberg (2013) · Zbl 06294355 · doi:10.1007/978-3-642-40196-1_4
[50] Zhang, L.: Decision algorithms for probabilistic simulations. Ph.D. thesis, Universität des Saarlandes, Saarbrücken (2009)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.