{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T03:26:54Z","timestamp":1777519614680,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":67,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642170706","type":"print"},{"value":"9783642170713","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-17071-3_16","type":"book-chapter","created":{"date-parts":[[2010,11,11]],"date-time":"2010-11-11T07:12:58Z","timestamp":1289459578000},"page":"311-337","source":"Crossref","is-referenced-by-count":25,"title":["The How and Why of Interactive Markov Chains"],"prefix":"10.1007","author":[{"given":"Holger","family":"Hermanns","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1006\/jcss.1999.1683","volume":"60","author":"C. Baier","year":"2000","unstructured":"Baier, C., Engelen, B., Majster-Cederbaum, M.E.: Deciding bisimilarity and similarity for probabilistic processes. Journal of Computer and System Sciences\u00a060, 187\u2013231 (2000)","journal-title":"Journal of Computer and System Sciences"},{"key":"16_CR2","first-page":"524","volume":"29","author":"C. Baier","year":"2003","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE TSE\u00a029, 524\u2013541 (2003)","journal-title":"IEEE TSE"},{"key":"16_CR3","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/j.ic.2005.03.001","volume":"200","author":"C. Baier","year":"2005","unstructured":"Baier, C., Katoen, J.-P., Hermanns, H., Wolf, V.: Comparative branching-time semantics for Markov chains. Information and Computation\u00a0200, 149\u2013214 (2005)","journal-title":"Information and Computation"},{"key":"16_CR4","unstructured":"Barendregt, H.: The quest for correctness. In: Images of SMC Research 1996. Stichting Mathematisch Centrum, pp. 39\u201358 (1996)"},{"key":"16_CR5","volume-title":"Handbook of Process Algebra","year":"2001","unstructured":"Bergstra, J.A., Ponse, A. (eds.): Handbook of Process Algebra. Elsevier Publishers B.V, Amsterdam (2001)"},{"key":"16_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0304-3975(97)00127-8","volume":"254","author":"M. Bernardo","year":"1998","unstructured":"Bernardo, M., Gorrieri, R.: Corrigendum to \u201cA tutorial on EMPA: A theory of concurrent processes with nondeterminism, priorities, probabilities and time. TCS 202\u00a0254, 1\u201354 (1998); Theoretical Computer Science 254, 691\u2013694 (2001)","journal-title":"TCS 202"},{"key":"16_CR7","volume-title":"Dynamic Programming and Optimal Control","author":"D. Bertsekas","year":"1995","unstructured":"Bertsekas, D.: Dynamic Programming and Optimal Control, vol.\u00a0II. Athena Scientific, Belmont (1995)"},{"key":"16_CR8","first-page":"274","volume":"35","author":"E. B\u00f6de","year":"2009","unstructured":"B\u00f6de, E., Herbstritt, M., Hermanns, H., Johr, S., Peikenkamp, T., Pulungan, R., Rakow, J., Wimmer, R., Becker, B.: Compositional dependability evaluation for STATEMATE. IEEE TSE\u00a035, 274\u2013292 (2009)","journal-title":"IEEE TSE"},{"key":"16_CR9","first-page":"512","volume-title":"Dependable Systems and Networks (DSN)","author":"H. Boudali","year":"2008","unstructured":"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\u2013521. IEEE, Los Alamitos (2008)"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-540-75596-8_31","volume-title":"Automated Technology for Verification and Analysis","author":"H. Boudali","year":"2007","unstructured":"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.\u00a04762, pp. 441\u2013456. Springer, Heidelberg (2007)"},{"key":"16_CR11","volume-title":"Dependable Systems and Networks (DSN)","author":"H. Boudali","year":"2007","unstructured":"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)"},{"key":"16_CR12","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1109\/TDSC.2009.45","volume":"7","author":"H. Boudali","year":"2009","unstructured":"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\u00a07, 128\u2013143 (2009)","journal-title":"IEEE Transactions on Secure and Dependable Computing"},{"key":"16_CR13","first-page":"121","volume-title":"Proc. 7th Int. Conf. on Formal Methods and Models for Co-Design MEMOCODE","author":"M. Bozzano","year":"2009","unstructured":"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\u2013130. IEEE CS Press, Los Alamitos (2009)"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-642-04468-7_15","volume-title":"Computer Safety, Reliability, and Security","author":"M. Bozzano","year":"2009","unstructured":"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.\u00a05775, pp. 173\u2013186. Springer, Heidelberg (2009)"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1093\/comjnl\/bxq024"},{"key":"16_CR16","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"107","volume-title":"Proceedings of the Workshop Essays on Algebraic Process Calculi.","author":"M. Bravetti","year":"2006","unstructured":"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.\u00a0162, pp. 107\u2013112. Elsevier, Amsterdam (2006)"},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/3-540-44667-2_5","volume-title":"Lectures on Formal Methods and Performance Analysis","author":"E. Brinksma","year":"2001","unstructured":"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.\u00a02090, pp. 183\u2013231. Springer, Heidelberg (2001)"},{"key":"16_CR18","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1017\/S0021900200107338","volume":"31","author":"P. Buchholz","year":"1994","unstructured":"Buchholz, P.: Exact and ordinary lumpability in finite markov chains. J. of Applied Probability\u00a031, 59\u201375 (1994)","journal-title":"J. of Applied Probability"},{"key":"16_CR19","volume-title":"IEEE International Workshop on Quantitative Evaluation of Large-Scale Systems and Technologies","author":"G. Chehaibar","year":"2009","unstructured":"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)"},{"key":"16_CR20","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/0166-5316(95)00008-L","volume":"24","author":"G. Chiola","year":"1995","unstructured":"Chiola, G., Franceschinis, G., Gaeta, R., Ribaudo, M.: GreatSPN 1.7: Graphical editor and analyzer for timed and stochastic Petri nets. Performance Evaluation\u00a024, 47\u201368 (1995)","journal-title":"Performance Evaluation"},{"key":"16_CR21","first-page":"270","volume-title":"ISSRE","author":"D. Coppit","year":"2000","unstructured":"Coppit, D., Sullivan, K.J., Dugan, J.B.: Formal semantics for computational engineering: A case study on dynamic fault trees. In: ISSRE, pp. 270\u2013282. IEEE Computer Society, Los Alamitos (2000)"},{"key":"16_CR22","first-page":"88","volume-title":"Design, Automation and Test in Europe (DATE)","author":"N. Coste","year":"2008","unstructured":"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\u201389. IEEE, Los Alamitos (2008)"},{"key":"16_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-642-02658-4_18","volume-title":"Computer Aided Verification","author":"N. Coste","year":"2009","unstructured":"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.\u00a05643, pp. 204\u2013218. Springer, Heidelberg (2009)"},{"key":"16_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/978-3-642-02930-1_36","volume-title":"Automata, Languages and Programming","author":"R. Nicola De","year":"2009","unstructured":"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.\u00a05556, pp. 435\u2013446. Springer, Heidelberg (2009)"},{"key":"16_CR25","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1109\/24.159800","volume":"41","author":"J. Dugan","year":"1992","unstructured":"Dugan, J., Bavuso, S., Boyd, M.: Dynamic fault-tree models for fault-tolerant computer systems. IEEE Transactions on Reliability\u00a041, 363\u2013377 (1992)","journal-title":"IEEE Transactions on Reliability"},{"key":"16_CR26","volume-title":"IEEE Symposium on Logic in Computer Science (LICS)","author":"C. Eisentraut","year":"2010","unstructured":"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)"},{"key":"16_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/11691617_5","volume-title":"Model Checking Software","author":"H. Fecher","year":"2006","unstructured":"Fecher, H., Leucker, M., Wolf, V.: Don\u2019t know in probabilistic systems. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol.\u00a03925, pp. 71\u201388. Springer, Heidelberg (2006)"},{"key":"16_CR28","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.21236\/ADA455842"},{"key":"16_CR29","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/151233.151241","volume":"36","author":"K.A. Frenkel","year":"1993","unstructured":"Frenkel, K.A., Milner, R.: An interview with Robin Milner. CACM\u00a036, 90\u201397 (1993)","journal-title":"CACM"},{"key":"16_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/3-540-45614-7_23","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"H. Garavel","year":"2002","unstructured":"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.\u00a02391, pp. 410\u2013429. Springer, Heidelberg (2002)"},{"key":"16_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-540-73368-3_18","volume-title":"Computer Aided Verification","author":"H. Garavel","year":"2007","unstructured":"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.\u00a04590, pp. 158\u2013163. Springer, Heidelberg (2007)"},{"key":"16_CR32","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1109\/32.922715","volume":"27","author":"S. Gilmore","year":"2001","unstructured":"Gilmore, S., Hillston, J., Ribaudo, M.: An efficient algorithm for aggregating PEPA models. IEEE Trans. Software Eng.\u00a027, 449\u2013464 (2001)","journal-title":"IEEE Trans. Software Eng."},{"key":"16_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-540-78929-1_18","volume-title":"Hybrid Systems: Computation and Control","author":"T. Han","year":"2008","unstructured":"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.\u00a04981, pp. 244\u2013258. Springer, Heidelberg (2008)"},{"key":"16_CR34","doi-asserted-by":"publisher","DOI":"10.1002\/0470841923","volume-title":"Performance of Computer Communication Systems: A Model-Based Approach","author":"B.R. Haverkort","year":"1998","unstructured":"Haverkort, B.R.: Performance of Computer Communication Systems: A Model-Based Approach. John Wiley & Sons, Chichester (1998)"},{"key":"16_CR35","series-title":"Lecture Notes in Computer Science","volume-title":"Interactive Markov Chains","year":"2002","unstructured":"Hermanns, H. (ed.): Interactive Markov Chains. LNCS, vol.\u00a02428. Springer, Heidelberg (2002)"},{"key":"16_CR36","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/S0304-3975(00)00305-4","volume":"274","author":"H. Hermanns","year":"2002","unstructured":"Hermanns, H., Herzog, U., Katoen, J.-P.: Process algebra for performance evaluation. Theoretical Computer Science\u00a0274, 43\u201387 (2002)","journal-title":"Theoretical Computer Science"},{"key":"16_CR37","first-page":"183","volume-title":"Petri Nets and Performance Models (PNPM)","author":"H. Hermanns","year":"1997","unstructured":"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\u2013192. IEEE, Los Alamitos (1997)"},{"key":"16_CR38","first-page":"718","volume-title":"Dependable Systems and Networks (DSN)","author":"H. Hermanns","year":"2007","unstructured":"Hermanns, H., Johr, S.: Uniformity by construction in the analysis of nondeterministic stochastic systems. In: Dependable Systems and Networks (DSN), pp. 718\u2013728. IEEE, Los Alamitos (2007)"},{"key":"16_CR39","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/S0167-6423(99)00019-2","volume":"36","author":"H. Hermanns","year":"2000","unstructured":"Hermanns, H., Katoen, J.-P.: Automated compositional Markov chain generation for a plain-old telephone system. Science of Comp. Progr.\u00a036, 97\u2013127 (2000)","journal-title":"Science of Comp. Progr."},{"key":"16_CR40","unstructured":"Hermanns, H., Katoen, J.-P., Neuh\u00e4u\u00dfer, M.R., Zhang, L.: GSPN model checking despite confusion. Technical report, RWTH Aachen University (2010)"},{"key":"16_CR41","unstructured":"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.\u00a027(4), Universit\u00e4t Erlangen (1994)"},{"key":"16_CR42","unstructured":"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\u2013140. VDE Verlag (May 2008)"},{"key":"16_CR43","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569951","volume-title":"A Compositional Approach to Performance Modelling","author":"J. Hillston","year":"1996","unstructured":"Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, Cambridge (1996)"},{"key":"16_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Hinton","year":"2006","unstructured":"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.\u00a03920, pp. 441\u2013444. Springer, Heidelberg (2006)"},{"key":"16_CR45","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1145\/828.833","volume":"31","author":"C. Hoare","year":"1984","unstructured":"Hoare, C., Brookes, S., Roscoe, A.: A theory of communicating sequential processes. J. ACM\u00a031, 560\u2013599 (1984)","journal-title":"J. ACM"},{"key":"16_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/3-540-54430-5_99","volume-title":"CONCUR \u201991","author":"B. Jonsson","year":"1991","unstructured":"Jonsson, B.: Simulations between specifications of distributed systems. In: Groote, J.F., Baeten, J.C.M. (eds.) CONCUR 1991. LNCS, vol.\u00a0527, pp. 346\u2013360. Springer, Heidelberg (1991)"},{"key":"16_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-71209-1_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.-P. Katoen","year":"2007","unstructured":"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.\u00a04424, pp. 87\u2013102. Springer, Heidelberg (2007)"},{"key":"16_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-540-73368-3_37","volume-title":"Computer Aided Verification","author":"J.-P. Katoen","year":"2007","unstructured":"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.\u00a04590, pp. 311\u2013324. Springer, Heidelberg (2007)"},{"key":"16_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-642-04368-0_16","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"J.-P. Katoen","year":"2009","unstructured":"Katoen, J.-P., Klink, D., Neuh\u00e4u\u00dfer, M.R.: Compositional abstraction for stochastic systems. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol.\u00a05813, pp. 195\u2013211. Springer, Heidelberg (2009)"},{"key":"16_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-540-78499-9_30","volume-title":"Foundations of Software Science and Computational Structures","author":"B. Klin","year":"2008","unstructured":"Klin, B., Sassone, V.: Structural operational semantics for stochastic process calculi. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol.\u00a04962, pp. 428\u2013442. Springer, Heidelberg (2008)"},{"key":"16_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-52148-8_19","volume-title":"Automatic Verification Methods for Finite State Systems","author":"K.G. Larsen","year":"1990","unstructured":"Larsen, K.G.: Modal specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407, pp. 232\u2013246. Springer, Heidelberg (1990)"},{"key":"16_CR52","first-page":"203","volume-title":"IEEE Symposium on Logic in Computer Science (LICS)","author":"K.G. Larsen","year":"1988","unstructured":"Larsen, K.G., Thomsen, B.: A modal process logic. In: IEEE Symposium on Logic in Computer Science (LICS), pp. 203\u2013210. IEEE, Los Alamitos (1988)"},{"key":"16_CR53","first-page":"219","volume":"2","author":"N.A. Lynch","year":"1989","unstructured":"Lynch, N.A., Tuttle, M.R.: An introduction to input\/output automata. CWI Quarterly\u00a02, 219\u2013246 (1989)","journal-title":"CWI Quarterly"},{"key":"16_CR54","doi-asserted-by":"publisher","first-page":"699","DOI":"10.1016\/0026-2714(91)90010-5","volume":"31","author":"M.A. Marsan","year":"1991","unstructured":"Marsan, M.A., Balbo, G., Chiola, G., Conte, G., Donatelli, S., Franceschinis, G.: An introduction to generalized stochastic Petri nets. Microelectronics and Reliability\u00a031, 699\u2013725 (1991)","journal-title":"Microelectronics and Reliability"},{"key":"16_CR55","volume-title":"Modelling with Generalized Stochastic Petri Nets","author":"M.A. Marsan","year":"1995","unstructured":"Marsan, M.A., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets. John Wiley & Sons, Chichester (1995)"},{"key":"16_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/978-3-540-74407-8_28","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"M.R. Neuh\u00e4u\u00dfer","year":"2007","unstructured":"Neuh\u00e4u\u00dfer, 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.\u00a04703, pp. 412\u2013427. Springer, Heidelberg (2007)"},{"key":"16_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-642-00596-1_26","volume-title":"Foundations of Software Science and Computational Structures","author":"M.R. Neuh\u00e4u\u00dfer","year":"2009","unstructured":"Neuh\u00e4u\u00dfer, M.R., Stoelinga, M., Katoen, J.-P.: Delayed nondeterminism in continuous-time Markov decision processes. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol.\u00a05504, pp. 364\u2013379. Springer, Heidelberg (2009)"},{"key":"16_CR58","unstructured":"Neuh\u00e4u\u00dfer, M.R.: Model Checking Nondeterministic and Randomly Timed Systems. PhD thesis, RWTH Aachen University \/ University of Twente (2010)"},{"key":"16_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-540-74974-5_20","volume-title":"Service-Oriented Computing \u2013 ICSOC 2007","author":"D. Prandi","year":"2007","unstructured":"Prandi, D., Quaglia, P.: Stochastic COWS. In: Kr\u00e4mer, B.J., Lin, K.-J., Narasimhan, P. (eds.) ICSOC 2007. LNCS, vol.\u00a04749, pp. 245\u2013256. Springer, Heidelberg (2007)"},{"key":"16_CR60","unstructured":"Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Laboratory for Computer Science, Massachusetts Institute of Technology (1995)"},{"key":"16_CR61","unstructured":"http:\/\/portal.acm.org\/citation.cfm?id=1451820"},{"key":"16_CR62","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/233551.233556","volume":"43","author":"R.J. Glabbeek van","year":"1996","unstructured":"van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. J. ACM\u00a043, 555\u2013600 (1996)","journal-title":"J. ACM"},{"key":"16_CR63","unstructured":"Veseley, W., Goldberg, F., Roberts, N., Haasl, D.: Fault Tree Handbook. US Nuclear Regulatory Commission, NUREG- 0492 (1981)"},{"key":"16_CR64","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/0304-3975(90)90111-T","volume":"89","author":"C. Vissers","year":"1991","unstructured":"Vissers, C., Scollo, G., van Sinderen, M., Brinksma, E.: On the use of specification styles in the design of distributed systems. Theor. Comput. Sci.\u00a089, 179\u2013206 (1991)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/11901914_35","volume-title":"Automated Technology for Verification and Analysis","author":"R. Wimmer","year":"2006","unstructured":"Wimmer, R., Herbstritt, M., Hermanns, H., Strampp, K., Becker, B.: Sigref \u2013 a symbolic bisimulation tool box. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol.\u00a04218, pp. 477\u2013492. Springer, Heidelberg (2006)"},{"key":"16_CR66","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-642-12002-2_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Zhang","year":"2010","unstructured":"Zhang, L., Neuh\u00e4u\u00dfer, 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.\u00a06015, pp. 53\u201368. Springer, Heidelberg (2010)"},{"key":"16_CR67","doi-asserted-by":"crossref","unstructured":"Zhang, L., Hermanns, H., Eisenbrand, F., Jansen, D.N.: Flow faster: Efficient decision algorithms for probabilistic simulations. Logical Methods in Computer Science\u00a04 (2008)","DOI":"10.2168\/LMCS-4(4:6)2008"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Components and Objects"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-17071-3_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T19:12:58Z","timestamp":1558293178000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-17071-3_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642170706","9783642170713"],"references-count":67,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-17071-3_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}