×

zbMATH — the first resource for mathematics

Compositional abstraction for stochastic systems. (English) Zbl 1262.68142
Ouaknine, Joël (ed.) et al., Formal modeling and analysis of timed systems. 7th international conference, FORMATS 2009, Budapest, Hungary, September 14–16, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-04367-3/pbk). Lecture Notes in Computer Science 5813, 195-211 (2009).
Summary: We propose to exploit three-valued abstraction to stochastic systems in a compositional way. This combines the strengths of an aggressive state-based abstraction technique with compositional modeling. Applying this principle to interactive Markov chains yields abstract models that combine interval Markov chains and modal transition systems in a natural and orthogonal way. We prove the correctness of our technique for parallel and symmetric composition and show that it yields lower bounds for minimal and upper bounds for maximal timed reachability probabilities.
For the entire collection see [Zbl 1176.68014].

MSC:
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
Software:
CADP; CEGAR; PEPA; SIGREF
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Baier, C., Hermanns, H., Katoen, J.-P., Haverkort, B.R.: Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Theor. Comput. Sci. 345, 2–26 (2005) · Zbl 1081.90066 · doi:10.1016/j.tcs.2005.07.022
[2] Berendsen, J., Vaandrager, F.W.: Compositional abstraction in real-time model checking. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 233–249. Springer, Heidelberg (2008) · Zbl 1171.68545 · doi:10.1007/978-3-540-85778-5_17
[3] Bode, E., Herbstritt, M., Hermanns, H., Johr, S., Peikenkamp, T., Pulungan, R., Wimmer, R., Becker, B.: Compositional performability evaluation for statemate. In: QEST, pp. 167–178. IEEE Computer Society Press, Los Alamitos (2006)
[4] Cardelli, L.: On process rate semantics. Theor. Comput. Sci. 391, 190–215 (2008) · Zbl 1133.68054 · doi:10.1016/j.tcs.2007.11.012
[5] Chadha, R., Viswanathan, M., Viswanathan, R.: Least upper bounds for probability measures and their applications to abstractions. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 264–278. Springer, Heidelberg (2008) · Zbl 1160.68436 · doi:10.1007/978-3-540-85361-9_23
[6] de Alfaro, L., Henzinger, T.A., Jhala, R.: Compositional methods for probabilistic systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 351–365. Springer, Heidelberg (2001) · Zbl 1006.68083 · doi:10.1007/3-540-44685-0_24
[7] 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
[8] 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
[9] Garavel, H., Hermanns, H.: On combining functional verification and performance evaluation using CADP. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 410–429. Springer, Heidelberg (2002) · Zbl 1064.68523 · doi:10.1007/3-540-45614-7_23
[10] Gilmore, S., Hillston, J., Ribaudo, M.: An efficient algorithm for aggregating PEPA models. IEEE Trans. Software Eng. 27, 449–464 (2001) · Zbl 05113721 · doi:10.1109/32.922715
[11] Hermanns, H., Johr, S.: Uniformity by construction in the analysis of nondeterministic stochastic systems. Dependable Systems and Networks, 718–728 (2007)
[12] Hermanns, H. (ed.): Interactive Markov Chains. LNCS, vol. 2428. Springer, Heidelberg (2002) · Zbl 1012.68142
[13] Hermanns, H., Herzog, U., Katoen, J.-P.: Process algebra for performance evaluation. Theor. Comput. Sci. 274, 43–87 (2002) · Zbl 0992.68149 · doi:10.1016/S0304-3975(00)00305-4
[14] Hermanns, H., Katoen, J.-P.: Automated compositional Markov chain generation for a plain-old telephone system. Sci. Comput. Program. 36, 97–127 (2000) · Zbl 0941.68649 · doi:10.1016/S0167-6423(99)00019-2
[15] Hermanns, H., Ribaudo, M.: Exploiting symmetries in stochastic process algebras. In: European Simulation Multiconference, SCS Europe, pp. 763–770 (1998)
[16] 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
[17] Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, Cambridge (1996) · Zbl 1080.68003 · doi:10.1017/CBO9780511569951
[18] Johr, S.: Model Checking Compositional Markov Systems. PhD thesis, Universität des Saarlandes, Saarbrücken, Germany (2007) · Zbl 1144.68040
[19] Jones, C., Plotkin, G.: A probabilistic powerdomain of evaluations. In: LICS, pp. 186–195. IEEE Computer Society, Los Alamitos (1989) · Zbl 0716.06003
[20] Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS, pp. 266–277. IEEE Computer Society, Los Alamitos (1991)
[21] Katoen, J.-P., Klink, D., Leucker, M., Wolf, V.: Three-valued abstraction for continuous-time Markov chains. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 311–324. Springer, Heidelberg (2007) · Zbl 1135.68476 · doi:10.1007/978-3-540-73368-3_37
[22] Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: Abstraction refinement for probabilistic software. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 182–197. Springer, Heidelberg (2009) · Zbl 1206.68090 · doi:10.1007/978-3-540-93900-9_17
[23] Kattenbelt, M., Kwiatkowska, M.Z., Norman, G., Parker, D.: Game-based probabilistic predicate abstraction in PRISM. ENTCS 220, 5–21 (2008) · Zbl 1286.68316
[24] Kwiatkowska, M., Norman, G., Parker, D.: Game-based abstraction for Markov decision processes. In: QEST, pp. 157–166. IEEE Computer Society Press, Los Alamitos (2006)
[25] Larsen, K.G., Thomsen, B.: A modal process logic. In: LICS, pp. 203–210. IEEE Computer Society Press, Los Alamitos (1988)
[26] Larsen, K.G.: Modal specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 232–246. Springer, Heidelberg (1990) · doi:10.1007/3-540-52148-8_19
[27] Maci, H., Valero, V., de Frutos-Escrig, D.: sPBC: A Markovian extension of finite Petri box calculus. Petri Nets and Performance Models, 207–216 (2001)
[28] Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. Nord. J. Comput. 2, 250–273 (1995) · Zbl 0839.68067
[29] Shoham, S., Grumberg, O.: Compositional verification and 3-valued abstractions join forces. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 69–86. Springer, Heidelberg (2007) · Zbl 1211.68256 · doi:10.1007/978-3-540-74061-2_5
[30] Shoham, S., Grumberg, O.: 3-valued abstraction: More precision at less cost. Inf. Comput. 206, 1313–1333 (2008) · Zbl 1169.68028 · doi:10.1016/j.ic.2008.07.004
[31] Tofts, C.M.N.: Compositional performance analysis. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 290–305. Springer, Heidelberg (1997) · doi:10.1007/BFb0035395
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.