×

zbMATH — the first resource for mathematics

The how and why of interactive Markov chains. (English) Zbl 1312.68152
de Boer, Frank S. (ed.) et al., Formal methods for components and objects. 8th international symposium, FMCO 2009, Eindhoven, The Netherlands, November 4–6, 2009. Revised selected papers. Berlin: Springer (ISBN 978-3-642-17070-6/pbk). Lecture Notes in Computer Science 6286, 311-337 (2010).
Summary: This paper reviews the model of interactive Markov chains (IMCs, for short), an extension of labelled transition systems with exponentially delayed transitions. We show that IMCs are closed under parallel composition and hiding, and show how IMCs can be compositionally aggregated prior to analysis by e.g., bisimulation minimisation or aggressive abstraction based on simulation pre-congruences. We survey some recent analysis techniques for IMCs, i.e., explaining how measures such as reachability probabilities can be obtained. Finally, we demonstrate that IMCs are a natural (and simple) semantic model for stochastic process algebras and generalised stochastic Petri nets and can be used for engineering formalisms such as AADL and dynamic fault trees.
For the entire collection see [Zbl 1203.68021].
Reviewer: Reviewer (Berlin)

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
60J20 Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.)
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Baier, C., Engelen, B., Majster-Cederbaum, M.E.: Deciding bisimilarity and similarity for probabilistic processes. Journal of Computer and System Sciences 60, 187–231 (2000) · Zbl 1073.68690 · doi:10.1006/jcss.1999.1683
[2] Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE TSE 29, 524–541 (2003)
[3] Baier, C., Katoen, J.-P., Hermanns, H., Wolf, V.: Comparative branching-time semantics for Markov chains. Information and Computation 200, 149–214 (2005) · Zbl 1101.68053 · doi:10.1016/j.ic.2005.03.001
[4] Barendregt, H.: The quest for correctness. In: Images of SMC Research 1996. Stichting Mathematisch Centrum, pp. 39–58 (1996)
[5] Bergstra, J.A., Ponse, A. (eds.): Handbook of Process Algebra. Elsevier Publishers B.V, Amsterdam (2001) · Zbl 0971.00006
[6] Bernardo, M., Gorrieri, R.: Corrigendum to ”A tutorial on EMPA: A theory of concurrent processes with nondeterminism, priorities, probabilities and time. TCS 202 254, 1–54 (1998); Theoretical Computer Science 254, 691–694 (2001) · Zbl 0902.68075 · doi:10.1016/S0304-3975(97)00127-8
[7] Bertsekas, D.: Dynamic Programming and Optimal Control, vol. II. Athena Scientific, Belmont (1995) · Zbl 0904.90170
[8] Böde, E., Herbstritt, M., Hermanns, H., Johr, S., Peikenkamp, T., Pulungan, R., Rakow, J., Wimmer, R., Becker, B.: Compositional dependability evaluation for STATEMATE. IEEE TSE 35, 274–292 (2009)
[9] Boudali, H., Crouzen, P., Haverkort, B.R., Kuntz, M., Stoelinga, M.I.A.: Architectural dependability evaluation with Arcade. In: Dependable Systems and Networks (DSN), pp. 512–521. IEEE, Los Alamitos (2008)
[10] Boudali, H., Crouzen, P., Stoelinga, M.: A compositional semantics for dynamic fault trees in terms of interactive Markov chains. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 441–456. Springer, Heidelberg (2007) · Zbl 1141.68454 · doi:10.1007/978-3-540-75596-8_31
[11] Boudali, H., Crouzen, P., Stoelinga, M.I.A.: Dynamic fault tree analysis using input/output interactive Markov chains. In: Dependable Systems and Networks (DSN). IEEE, Los Alamitos (2007) · Zbl 1141.68454
[12] Boudali, H., Crouzen, P., Stoelinga, M.I.A.: Rigorous, compositional, and extensible framework for dynamic fault tree analysis. IEEE Transactions on Secure and Dependable Computing 7, 128–143 (2009) · doi:10.1109/TDSC.2009.45
[13] Bozzano, M., Cimatti, A., Katoen, J.-P., Nguyen, V., Noll, T., Roveri, M.: Codesign of dependable systems: A component-based modelling language. In: Proc. 7th Int. Conf. on Formal Methods and Models for Co-Design MEMOCODE, pp. 121–130. IEEE CS Press, Los Alamitos (2009)
[14] Bozzano, M., Cimatti, A., Katoen, J.-P., Nguyen, V., Noll, T., Roveri, M.: The COMPASS approach: Correctness, modelling and performability of aerospace systems. In: Buth, B., Rabe, G., Seyfarth, T. (eds.) SAFECOMP 2009. LNCS, vol. 5775, pp. 173–186. Springer, Heidelberg (2009) · Zbl 05615935 · doi:10.1007/978-3-642-04468-7_15
[15] Bozzano, M., Cimatti, A., Katoen, J.-P., Nguyen, V., Noll, T., Roveri, M.: Safety, dependability and performance analysis of extended AADL models. The Computer Journal (2010)
[16] Bravetti, M., Hermanns, H., Katoen, J.-P.: YMCA: Why Markov chain algebra? In: Proceedings of the Workshop Essays on Algebraic Process Calculi. Electronic Notes in Theoretical Computer Science, vol. 162, pp. 107–112. Elsevier, Amsterdam (2006) · Zbl 1316.68088
[17] Brinksma, E., Hermanns, H.: Process Algebra and Markov Chains. In: Brinksma, E., Hermanns, H., Katoen, J.-P. (eds.) EEF School 2000 and FMPA 2000. LNCS, vol. 2090, pp. 183–231. Springer, Heidelberg (2001) · Zbl 0990.68021 · doi:10.1007/3-540-44667-2_5
[18] Buchholz, P.: Exact and ordinary lumpability in finite markov chains. J. of Applied Probability 31, 59–75 (1994) · Zbl 0796.60073 · doi:10.1017/S0021900200107338
[19] Chehaibar, G., Zidouni, M., Mateescu, R.: Modeling multiprocessor cache protocol impact on MPI performance. In: IEEE International Workshop on Quantitative Evaluation of Large-Scale Systems and Technologies. IEEE, Los Alamitos (2009)
[20] Chiola, G., Franceschinis, G., Gaeta, R., Ribaudo, M.: GreatSPN 1.7: Graphical editor and analyzer for timed and stochastic Petri nets. Performance Evaluation 24, 47–68 (1995) · Zbl 0875.68663 · doi:10.1016/0166-5316(95)00008-L
[21] Coppit, D., Sullivan, K.J., Dugan, J.B.: Formal semantics for computational engineering: A case study on dynamic fault trees. In: ISSRE, pp. 270–282. IEEE Computer Society, Los Alamitos (2000)
[22] Coste, N., Garavel, H., Hermanns, H., Hersemeule, R., Thonnart, Y., Zidouni, M.: Quantitative evaluation in embedded system design: Validation of multiprocessor multithreaded architectures. In: Design, Automation and Test in Europe (DATE), pp. 88–89. IEEE, Los Alamitos (2008)
[23] Coste, N., Hermanns, H., Lantreibecq, E., Serwe, W.: Towards performance prediction of compositional models in industrial GALS designs. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification. LNCS, vol. 5643, pp. 204–218. Springer, Heidelberg (2009) · Zbl 1242.68005 · doi:10.1007/978-3-642-02658-4_18
[24] De Nicola, R., Latella, D., Loreti, M., Massink, M.: Rate-based transition systems for stochastic process calculi. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009. LNCS, vol. 5556, pp. 435–446. Springer, Heidelberg (2009) · Zbl 1248.68350 · doi:10.1007/978-3-642-02930-1_36
[25] Dugan, J., Bavuso, S., Boyd, M.: Dynamic fault-tree models for fault-tolerant computer systems. IEEE Transactions on Reliability 41, 363–377 (1992) · Zbl 0825.68162 · doi:10.1109/24.159800
[26] Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: IEEE Symposium on Logic in Computer Science (LICS). IEEE, Los Alamitos (2010) · Zbl 1287.68132
[27] 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
[28] Feiler, P.H., Rugina, A.: Dependability modeling with the Architecture Analysis & Design Language (AADL). Technical Note CMU/SEI-2007-TN-043, CMU Software Engineering Institute (2007)
[29] Frenkel, K.A., Milner, R.: An interview with Robin Milner. CACM 36, 90–97 (1993) · doi:10.1145/151233.151241
[30] 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
[31] Garavel, H., Mateescu, R., Lang, F., Serwe, W.: CADP 2006: A toolbox for the construction and analysis of distributed processes. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 158–163. Springer, Heidelberg (2007) · Zbl 05216223 · doi:10.1007/978-3-540-73368-3_18
[32] 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
[33] Han, T., Katoen, J.-P., Mereacre, A.: Compositional modeling and minimization of time-inhomogeneous Markov chains. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 244–258. Springer, Heidelberg (2008) · Zbl 1144.93379 · doi:10.1007/978-3-540-78929-1_18
[34] Haverkort, B.R.: Performance of Computer Communication Systems: A Model-Based Approach. John Wiley & Sons, Chichester (1998) · doi:10.1002/0470841923
[35] Hermanns, H. (ed.): Interactive Markov Chains. LNCS, vol. 2428. Springer, Heidelberg (2002) · Zbl 1012.68142
[36] Hermanns, H., Herzog, U., Katoen, J.-P.: Process algebra for performance evaluation. Theoretical Computer Science 274, 43–87 (2002) · Zbl 0992.68149 · doi:10.1016/S0304-3975(00)00305-4
[37] Hermanns, H., Herzog, U., Mertsiotakis, V., Rettelbach, M.: Exploiting stochastic process algebra achievements for generalized stochastic Petri nets. In: Petri Nets and Performance Models (PNPM), pp. 183–192. IEEE, Los Alamitos (1997)
[38] Hermanns, H., Johr, S.: Uniformity by construction in the analysis of nondeterministic stochastic systems. In: Dependable Systems and Networks (DSN), pp. 718–728. IEEE, Los Alamitos (2007)
[39] Hermanns, H., Katoen, J.-P.: Automated compositional Markov chain generation for a plain-old telephone system. Science of Comp. Progr. 36, 97–127 (2000) · Zbl 0941.68649 · doi:10.1016/S0167-6423(99)00019-2
[40] Hermanns, H., Katoen, J.-P., Neuhäußer, M.R., Zhang, L.: GSPN model checking despite confusion. Technical report, RWTH Aachen University (2010)
[41] Hermanns, H., Rettelbach, M.: Syntax, Semantics, Equivalences, and Axioms for MTIPP. In: Herzog, U., Rettelbach, M. (eds.) Proc. of the 2nd Int. Workshop on Process Algebras and Performance Modelling. Arbeitsberichte des IMMD, vol. 27(4), Universität Erlangen (1994)
[42] Hermanns, H., Johr, S.: we reach it? or must we? in what time? with what probability? In: Measurement, Modelling and Evaluation of Computer and Communication Systems (MMB), pp. 125–140. VDE Verlag (May 2008)
[43] Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, Cambridge (1996) · Zbl 1080.68003 · doi:10.1017/CBO9780511569951
[44] Hinton, A., Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006) · doi:10.1007/11691372_29
[45] Hoare, C., Brookes, S., Roscoe, A.: A theory of communicating sequential processes. J. ACM 31, 560–599 (1984) · Zbl 0628.68025 · doi:10.1145/828.833
[46] Jonsson, B.: Simulations between specifications of distributed systems. In: Groote, J.F., Baeten, J.C.M. (eds.) CONCUR 1991. LNCS, vol. 527, pp. 346–360. Springer, Heidelberg (1991) · doi:10.1007/3-540-54430-5_99
[47] Katoen, J.-P., Kemna, T., Zapreev, I.S., Jansen, D.N.: Bisimulation minimisation mostly speeds up probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 87–102. Springer, Heidelberg (2007) · Zbl 1186.68296 · doi:10.1007/978-3-540-71209-1_9
[48] 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
[49] Katoen, J.-P., Klink, D., Neuhäußer, M.R.: Compositional abstraction for stochastic systems. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol. 5813, pp. 195–211. Springer, Heidelberg (2009) · Zbl 1262.68142 · doi:10.1007/978-3-642-04368-0_16
[50] Klin, B., Sassone, V.: Structural operational semantics for stochastic process calculi. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 428–442. Springer, Heidelberg (2008) · Zbl 1138.68468 · doi:10.1007/978-3-540-78499-9_30
[51] 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
[52] Larsen, K.G., Thomsen, B.: A modal process logic. In: IEEE Symposium on Logic in Computer Science (LICS), pp. 203–210. IEEE, Los Alamitos (1988)
[53] Lynch, N.A., Tuttle, M.R.: An introduction to input/output automata. CWI Quarterly 2, 219–246 (1989) · Zbl 0677.68067
[54] Marsan, M.A., Balbo, G., Chiola, G., Conte, G., Donatelli, S., Franceschinis, G.: An introduction to generalized stochastic Petri nets. Microelectronics and Reliability 31, 699–725 (1991) · doi:10.1016/0026-2714(91)90010-5
[55] Marsan, M.A., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets. John Wiley & Sons, Chichester (1995) · Zbl 0843.68080
[56] Neuhäußer, M.R., Katoen, J.-P.: Bisimulation and logical preservation for continuous-time Markov decision processes. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 412–427. Springer, Heidelberg (2007) · Zbl 1151.68549 · doi:10.1007/978-3-540-74407-8_28
[57] Neuhäußer, M.R., Stoelinga, M., Katoen, J.-P.: Delayed nondeterminism in continuous-time Markov decision processes. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 364–379. Springer, Heidelberg (2009) · Zbl 1234.68320 · doi:10.1007/978-3-642-00596-1_26
[58] Neuhäußer, M.R.: Model Checking Nondeterministic and Randomly Timed Systems. PhD thesis, RWTH Aachen University / University of Twente (2010)
[59] Prandi, D., Quaglia, P.: Stochastic COWS. In: Krämer, B.J., Lin, K.-J., Narasimhan, P. (eds.) ICSOC 2007. LNCS, vol. 4749, pp. 245–256. Springer, Heidelberg (2007) · Zbl 05304286 · doi:10.1007/978-3-540-74974-5_20
[60] Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Laboratory for Computer Science, Massachusetts Institute of Technology (1995)
[61] http://portal.acm.org/citation.cfm?id=1451820
[62] van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. J. ACM 43, 555–600 (1996) · Zbl 0882.68085 · doi:10.1145/233551.233556
[63] Veseley, W., Goldberg, F., Roberts, N., Haasl, D.: Fault Tree Handbook. US Nuclear Regulatory Commission, NUREG- 0492 (1981)
[64] Vissers, C., Scollo, G., van Sinderen, M., Brinksma, E.: On the use of specification styles in the design of distributed systems. Theor. Comput. Sci. 89, 179–206 (1991) · Zbl 0772.68065 · doi:10.1016/0304-3975(90)90111-T
[65] 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
[66] Zhang, L., Neuhäußer, M.R.: Model checking interactive Markov chains. In: Esparza, J., Majumdar, R. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 6015, pp. 53–68. Springer, Heidelberg (2010) · Zbl 1284.68420 · doi:10.1007/978-3-642-12002-2_5
[67] Zhang, L., Hermanns, H., Eisenbrand, F., Jansen, D.N.: Flow faster: Efficient decision algorithms for probabilistic simulations. Logical Methods in Computer Science 4 (2008) · Zbl 1161.68473 · doi:10.2168/LMCS-4(4:6)2008
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.