{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:16:40Z","timestamp":1759637800165},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642402128"},{"type":"electronic","value":"9783642402135"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40213-5_16","type":"book-chapter","created":{"date-parts":[[2013,8,29]],"date-time":"2013-08-29T09:26:23Z","timestamp":1377768383000},"page":"250-266","source":"Crossref","is-referenced-by-count":7,"title":["Improving Time Bounded Reachability Computations in Interactive Markov Chains"],"prefix":"10.1007","author":[{"given":"Hassan","family":"Hatefi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,8,30]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Towards Performance Prediction of Verifying Continuous Time Markov Chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 269\u2013276. Springer, Heidelberg (1996)","DOI":"10.1007\/3-540-61474-5_75"},{"issue":"6","key":"16_CR2","doi-asserted-by":"crossref","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C. Baier","year":"2003","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering 29(6), 524\u2013541 (2003)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"16_CR3","doi-asserted-by":"crossref","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.: Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Theoretical Computer Science 345, 2\u201326 (2005)","journal-title":"Theoretical Computer Science"},{"key":"16_CR4","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press (2008)"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499\u2013513. Springer, Heidelberg (1995)","DOI":"10.21236\/ADA461346"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Boudali, H., Crouzen, P., Haverkort, B.R., Kuntz, M., Stoelinga, M.: Architectural dependability evaluation with Arcade. In: DSN, pp. 512\u2013521. IEEE (2008)","DOI":"10.1109\/DSN.2008.4630122"},{"issue":"2","key":"16_CR7","doi-asserted-by":"crossref","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 Transactions on Software Engineering 35(2), 274\u2013292 (2009)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Bravetti, M., Hermanns, H., Katoen, J.-P.: YMCA - Why Markov Chain Algebra? Electronic Notes in Theoretical Computer Science 162, 107\u2013112 (2006)","DOI":"10.1016\/j.entcs.2005.12.108"},{"key":"16_CR9","unstructured":"Br\u00e1zdil, T., Hermanns, H., Kr\u010d\u00e1l, J., K\u0159et\u00ednsk\u00fd, J., \u0158eh\u00e1k, V.: Verification of Open Interactive Markov Chains. In: FSTTCS, pp. 474\u2013485 (2012)"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Cloth, L., Haverkort, B.R.: Model Checking for Survivability. In: QEST, pp. 145\u2013154. IEEE (2005)","DOI":"10.1109\/QEST.2005.21"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Coppersmith, D., Winograd, S.: Matrix Multiplication via Arithmetic Progressions. In: STOC, pp. 1\u20136 (1987)","DOI":"10.1145\/28395.28396"},{"key":"16_CR12","doi-asserted-by":"crossref","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.) CAV 2009. LNCS, vol. 5643, pp. 204\u2013218. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-02658-4_18"},{"key":"16_CR13","doi-asserted-by":"crossref","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 (2008)","DOI":"10.1145\/1403375.1403399"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Deng, Y., Hennessy, M.: On the Semantics of Markov Automata. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol. 6756, pp. 307\u2013318. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-22012-8_24"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: On Probabilistic Automata in Continuous Time. In: LICS, pp. 342\u2013351 (2010)","DOI":"10.1109\/LICS.2010.41"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Esteve, M.-A., Katoen, J.-P., Nguyen, V.Y., Postma, B., Yushtein, Y.: Formal correctness, safety, dependability and performance analysis of a satellite. In: ICSE, pp. 1022\u20131031 (2012)","DOI":"10.1109\/ICSE.2012.6227118"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 372\u2013387. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-19835-9_33"},{"key":"16_CR18","unstructured":"Guck, D.: Quantitative Analysis of Markov Automata. Master Thesis, RWTH Aachen University (2012)"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Guck, D., Han, T., Katoen, J.-P., Neuh\u00e4u\u00dfer, M.R.: Quantitative Timed Analysis of Interactive Markov Chains. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 8\u201323. Springer, Heidelberg (2012)","DOI":"10.1007\/978-3-642-28891-3_4"},{"key":"16_CR20","unstructured":"Hatefi, H., Hermanns, H.: Model Checking Algorithms for Markov Automata. ECEASST 53 (2012)"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"Hermanns, H.: Interactive Markov Chains. LNCS, vol. 2428. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-45804-2"},{"issue":"1\u20132","key":"16_CR22","doi-asserted-by":"crossref","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 274(1\u20132), pp. 43\u201387 (2002)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"16_CR23","doi-asserted-by":"crossref","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 Computer Programming 36(1), pp. 97\u2013127 (2000)","journal-title":"Science of Computer Programming"},{"key":"16_CR24","doi-asserted-by":"crossref","unstructured":"Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press (1996)","DOI":"10.1017\/CBO9780511569951"},{"key":"16_CR25","unstructured":"Maci\u00e0, H., Valero, V., Cuartero, F., Carmen Ruiz, M.: sPBC: A Markovian Extension of Petri Box Calculus with Immediate Multiactions. Fundamenta Informaticae 87(3\u20134), pp. 367\u2013406 (2008)"},{"key":"16_CR26","unstructured":"Neuh\u00e4usser, M.R.: Model Checking Nondeterministic and Randomly Timed Systems. PhD Thesis, RWTH Aachen University and University of Twente (2010)"},{"key":"16_CR27","doi-asserted-by":"crossref","unstructured":"Haverkort, B.R., Kuntz, M., Remke, A., Roolvink, S., Stoelinga, M.: Evaluating repair strategies for a water-treatment facility using Arcade. In: DSN, pp. 419\u2013424 (2010)","DOI":"10.1109\/DSN.2010.5544290"},{"key":"16_CR28","unstructured":"Pulungan, R.: Reduction of Acyclic Phase-Type Representations. PhD thesis, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany (2009)"},{"key":"16_CR29","doi-asserted-by":"crossref","unstructured":"Zhang, L., Neuh\u00e4usser, M.R.: Model Checking Interactive Markov Chains. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 53\u201368. Springer, Heidelberg (2010)","DOI":"10.1007\/978-3-642-12002-2_5"},{"key":"16_CR30","doi-asserted-by":"crossref","unstructured":"Zhang, L., Jansen, D.N., Nielson, F., Hermanns, H.: Automata-Based CSL Model Checking. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol. 6756, pp. 271\u2013282. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-22012-8_21"}],"container-title":["Lecture Notes in Computer Science","Fundamentals of Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40213-5_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T00:34:36Z","timestamp":1558053276000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40213-5_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642402128","9783642402135"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40213-5_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}