{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T03:32:43Z","timestamp":1777519963639,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642120015","type":"print"},{"value":"9783642120022","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-12002-2_5","type":"book-chapter","created":{"date-parts":[[2010,3,8]],"date-time":"2010-03-08T01:20:25Z","timestamp":1268011225000},"page":"53-68","source":"Crossref","is-referenced-by-count":29,"title":["Model Checking Interactive Markov Chains"],"prefix":"10.1007","author":[{"given":"Lijun","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin R.","family":"Neuh\u00e4u\u00dfer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","volume-title":"Probability & Measure Theory","author":"R. Ash","year":"2000","unstructured":"Ash, R., Dol\u00e9ans-Dade, C.: Probability & Measure Theory, 2nd edn. Academic Press, London (2000)","edition":"2"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/3-540-61474-5_75","volume-title":"Computer Aided Verification","author":"A. Aziz","year":"1996","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.K.: Verifying continuous time Markov chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 269\u2013276. Springer, Heidelberg (1996)"},{"key":"5_CR3","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":"5_CR4","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2005.07.022","volume":"345","author":"C. Baier","year":"2005","unstructured":"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. Comp. Sci.\u00a0345, 2\u201326 (2005)","journal-title":"Theor. Comp. Sci."},{"key":"5_CR5","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":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"A. Bianco","year":"1995","unstructured":"Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol.\u00a01026, pp. 499\u2013513. Springer, Heidelberg (1995)"},{"key":"5_CR7","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1109\/TSE.2008.102","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 Trans. Software Eng.\u00a035, 274\u2013292 (2009)","journal-title":"IEEE Trans. Software Eng."},{"key":"5_CR8","first-page":"512","volume-title":"DSN","author":"H. Boudali","year":"2008","unstructured":"Boudali, H., Crouzen, P., Haverkort, B.R., Kuntz, M., Stoelinga, M.: Architectural dependability evaluation with Arcade. In: DSN, pp. 512\u2013521. IEEE, Los Alamitos (2008)"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-02930-1_9","volume-title":"Automata, Languages and Programming","author":"P. Bouyer","year":"2009","unstructured":"Bouyer, P., Forejt, V.: Reachability in stochastic timed games. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009. LNCS, vol.\u00a05556, pp. 103\u2013114. Springer, Heidelberg (2009)"},{"key":"5_CR10","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"107","volume-title":"Essays on Algebraic Process Calculi","author":"M. Bravetti","year":"2006","unstructured":"Bravetti, M., Hermanns, H., Katoen, J.-P.: YMCA: Why Markov chain algebra? In: Essays on Algebraic Process Calculi. Electronic Notes in Theoretical Computer Science, vol.\u00a0162, pp. 107\u2013112. Elsevier, Amsterdam (2006)"},{"key":"5_CR11","unstructured":"Brazdil, T., Forejt, V., Krcal, J., Kretinsky, J., Kucera, A.: Continuous-time stochastic games with time-bounded reachability. In: FSTTCS. LIPIcs (2009) (to appear)"},{"key":"5_CR12","first-page":"199","volume-title":"QEST","author":"D. Cerotti","year":"2006","unstructured":"Cerotti, D., Donatelli, S., Horv\u00e1th, A., Sproston, J.: CSL model checking for generalized stochastic Petri nets. In: QEST, pp. 199\u2013210. IEEE, Los Alamitos (2006)"},{"key":"5_CR13","volume-title":"ACM Symposium on Theory of Computing","author":"D. Coppersmith","year":"1987","unstructured":"Coppersmith, D., Winograd, S.: Matrix multiplication via arithmetic progressions. In: ACM Symposium on Theory of Computing. ACM, New York (1987)"},{"key":"5_CR14","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1145\/1403375.1403399","volume-title":"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: DATE, pp. 88\u201389. IEEE, Los Alamitos (2008)"},{"key":"5_CR15","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":"5_CR16","first-page":"228","volume-title":"Reliable Distributed Systems","author":"B.R. Haverkort","year":"2000","unstructured":"Haverkort, B.R., Hermanns, H., Katoen, J.-P.: On the use of model checking techniques for dependability evaluation. In: Reliable Distributed Systems, pp. 228\u2013239. IEEE, Los Alamitos (2000)"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","volume-title":"Interactive Markov Chains","year":"2002","unstructured":"Hermanns, H. (ed.): Interactive Markov Chains: The Quest for Quantified Quality. LNCS, vol.\u00a02428. Springer, Heidelberg (2002)"},{"key":"5_CR18","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. Theor. Comp. Sci.\u00a0274, 43\u201387 (2002)","journal-title":"Theor. Comp. Sci."},{"key":"5_CR19","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. Sci. Comput. Program.\u00a036, 97\u2013127 (2000)","journal-title":"Sci. Comput. Program."},{"key":"5_CR20","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":"5_CR21","unstructured":"Johr, S.: Model Checking Compositional Markov Systems. PhD thesis, Saarland University, Saarbr\u00fccken, Germany (2007)"},{"key":"5_CR22","doi-asserted-by":"crossref","first-page":"367","DOI":"10.3233\/FUN-2008-873-405","volume":"87","author":"H. Maci\u00e1","year":"2008","unstructured":"Maci\u00e1, H., Valero, V., Cuartero, F., Ruiz, M.C.: sPBC: A Markovian extension of Petri box calculus with immediate multiactions. Fundamenta Informaticae\u00a087, 367\u2013406 (2008)","journal-title":"Fundamenta Informaticae"},{"key":"5_CR23","unstructured":"Neuh\u00e4u\u00dfer, M.R.: Model Checking Nondeterministic and Randomly Timed Systems. PhD thesis, RWTH Aachen University, Aachen, Germany (2010)"},{"key":"5_CR24","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":"5_CR25","doi-asserted-by":"crossref","unstructured":"Neuh\u00e4u\u00dfer, M.R., Zhang, L.: Time-bounded reachability in continuous-time Markov decision processes. Technical report, RWTH Aachen University (2009)","DOI":"10.1109\/QEST.2010.47"},{"key":"5_CR26","unstructured":"Pulungan, R.: Reduction of Acyclic Phase-Type Representations. PhD thesis, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany (2009)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-12002-2_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T01:39:06Z","timestamp":1739929146000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-12002-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642120015","9783642120022"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-12002-2_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}