{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,26]],"date-time":"2025-07-26T09:34:51Z","timestamp":1753522491761},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642401954"},{"type":"electronic","value":"9783642401961"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40196-1_5","type":"book-chapter","created":{"date-parts":[[2013,7,23]],"date-time":"2013-07-23T01:54:56Z","timestamp":1374544496000},"page":"55-71","source":"Crossref","is-referenced-by-count":31,"title":["Modelling, Reduction and Analysis of Markov Automata"],"prefix":"10.1007","author":[{"given":"Dennis","family":"Guck","sequence":"first","affiliation":[]},{"given":"Hassan","family":"Hatefi","sequence":"additional","affiliation":[]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[]},{"given":"Mark","family":"Timmer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"6","key":"5_CR1","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(6), 524\u2013541 (2003)","journal-title":"IEEE TSE"},{"issue":"3","key":"5_CR2","doi-asserted-by":"publisher","first-page":"580","DOI":"10.1287\/moor.16.3.580","volume":"16","author":"D.P. Bertsekas","year":"1991","unstructured":"Bertsekas, D.P., Tsitsiklis, J.N.: An analysis of stochastic shortest path problems. Mathematics of Operations Research\u00a016(3), 580\u2013595 (1991)","journal-title":"Mathematics of Operations Research"},{"issue":"2","key":"5_CR3","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1109\/TDSC.2009.45","volume":"7","author":"H. Boudali","year":"2010","unstructured":"Boudali, H., Crouzen, P., Stoelinga, M.I.A.: A rigorous, compositional, and extensible framework for dynamic fault tree analysis. IEEE Trans. Dependable Sec. Comput.\u00a07(2), 128\u2013143 (2010)","journal-title":"IEEE Trans. Dependable Sec. Comput."},{"issue":"5","key":"5_CR4","doi-asserted-by":"publisher","first-page":"754","DOI":"10.1093\/comjnl\/bxq024","volume":"54","author":"M. Bozzano","year":"2011","unstructured":"Bozzano, M., Cimatti, A., Katoen, J.-P., Nguyen, V.Y., Noll, T., Roveri, M.: Safety, dependability and performance analysis of extended AADL models. The Computer Journal\u00a054(5), 754\u2013775 (2011)","journal-title":"The Computer Journal"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, M.: Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification. In: SODA, pp. 1318\u20131336. SIAM (2011)","DOI":"10.1137\/1.9781611973082.101"},{"key":"5_CR6","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.) CAV 2009. LNCS, vol.\u00a05643, pp. 204\u2013218. Springer, Heidelberg (2009)"},{"key":"5_CR7","unstructured":"de Alfaro, L.: Formal Verification of Probabilistic Systems. PhD thesis, Stanford University (1997)"},{"key":"5_CR8","unstructured":"de Alfaro, L.: How to specify and verify the long-run average behavior of probabilistic systems. In: LICS, pp. 454\u2013465. IEEE (1998)"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/3-540-48320-9_7","volume-title":"CONCUR\u201999. Concurrency Theory","author":"L. Alfaro de","year":"1999","unstructured":"de Alfaro, L.: Computing minimum and maximum reachability times in probabilistic systems. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664, pp. 66\u201381. Springer, Heidelberg (1999)"},{"key":"5_CR10","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/j.ic.2012.10.010","volume":"222","author":"Y. Deng","year":"2013","unstructured":"Deng, Y., Hennessy, M.: On the semantics of Markov automata. Inf. Comput.\u00a0222, 139\u2013168 (2013)","journal-title":"Inf. Comput."},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1007\/978-3-642-38697-8_6","volume-title":"ICATPN 2013","author":"C. Eisentraut","year":"2013","unstructured":"Eisentraut, C., Hermanns, H., Katoen, J.-P., Zhang, L.: A semantics for every GSPN. In: Colom, J.-M., Desel, J. (eds.) ICATPN 2013. LNCS, vol.\u00a07927, pp. 90\u2013109. Springer, Heidelberg (2013)"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-642-15375-4_3","volume-title":"CONCUR 2010 - Concurrency Theory","author":"C. Eisentraut","year":"2010","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: Concurrency and composition in a stochastic world. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol.\u00a06269, pp. 21\u201339. Springer, Heidelberg (2010)"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: LICS, pp. 342\u2013351. IEEE (2010)","DOI":"10.1109\/LICS.2010.41"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/978-3-642-28891-3_4","volume-title":"NASA Formal Methods","author":"D. Guck","year":"2012","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.\u00a07226, pp. 8\u201323. Springer, Heidelberg (2012)"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Guck, D., Hatefi, H., Hermanns, H., Katoen, J.-P., Timmer, M.: Modelling, reduction and analysis of Markov automata (extended version). Technical Report 1305.7050, ArXiv e-prints (2013)","DOI":"10.1007\/978-3-642-40196-1_5"},{"key":"5_CR16","unstructured":"Hatefi, H., Hermanns, H.: Model checking algorithms for Markov automata. In: ECEASST (AVoCS proceedings), vol.\u00a053 (2012) (to appear)"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Haverkort, B.R., Kuntz, M., Remke, A., Roolvink, S., Stoelinga, M.I.A.: Evaluating repair strategies for a water-treatment facility using Arcade. In: DSN, pp. 419\u2013424. IEEE (2010)","DOI":"10.1109\/DSN.2010.5544290"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Hermanns, H.: Interactive Markov Chains: The Quest for Quantified Quality. LNCS, vol.\u00a02428. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-45804-2_5"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Katoen, J.-P.: GSPNs revisited: Simple semantics and new analysis algorithms. In: ACSD, pp. 6\u201311. IEEE (2012)","DOI":"10.1109\/ACSD.2012.30"},{"issue":"1","key":"5_CR20","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1016\/j.tcs.2011.07.021","volume":"413","author":"J.-P. Katoen","year":"2012","unstructured":"Katoen, J.-P., van de Pol, J.C., Stoelinga, M.I.A., Timmer, M.: A linear process-algebraic format with data for probabilistic automata. TCS\u00a0413(1), 36\u201357 (2012)","journal-title":"TCS"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/3-540-44804-7_4","volume-title":"Process Algebra and Probabilistic Methods. Performance Modelling and Verification","author":"G.G.I. L\u00f3pez","year":"2001","unstructured":"L\u00f3pez, G.G.I., Hermanns, H., Katoen, J.-P.: Beyond memoryless distributions: Model checking semi-markov chains. In: de Luca, L., Gilmore, S. (eds.) PAPM-PROBMIV 2001. LNCS, vol.\u00a02165, pp. 57\u201370. Springer, Heidelberg (2001)"},{"key":"5_CR22","unstructured":"Ajmone Marsan, M., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets. John Wiley & Sons (1995)"},{"issue":"2","key":"5_CR23","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1145\/190.191","volume":"2","author":"M. Ajmone Marsan","year":"1984","unstructured":"Ajmone Marsan, M., Conte, G., Balbo, G.: A class of generalized stochastic Petri nets for the performance evaluation of multiprocessor systems. ACM Transactions on Computer Systems\u00a02(2), 93\u2013122 (1984)","journal-title":"ACM Transactions on Computer Systems"},{"key":"5_CR24","unstructured":"Meyer, J.F., Movaghar, A., Sanders, W.H.: Stochastic activity networks: Structure, behavior, and application. In: PNPM, pp. 106\u2013115. IEEE (1985)"},{"key":"5_CR25","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.I.A., 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_CR26","unstructured":"Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, MIT (1995)"},{"issue":"6","key":"5_CR27","doi-asserted-by":"publisher","first-page":"667","DOI":"10.1287\/mnsc.37.6.667","volume":"37","author":"M.M. Srinivasan","year":"1991","unstructured":"Srinivasan, M.M.: Nondeterministic polling systems. Management Science\u00a037(6), 667\u2013681 (1991)","journal-title":"Management Science"},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"Timmer, M.: SCOOP: A tool for symbolic optimisations of probabilistic processes. In: QEST, pp. 149\u2013150. IEEE (2011)","DOI":"10.1109\/QEST.2011.27"},{"key":"5_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-642-32940-1_26","volume-title":"CONCUR 2012 \u2013 Concurrency Theory","author":"M. Timmer","year":"2012","unstructured":"Timmer, M., Katoen, J.-P., van de Pol, J.C., Stoelinga, M.I.A.: Efficient modelling and generation of Markov automata. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol.\u00a07454, pp. 364\u2013379. Springer, Heidelberg (2012)"},{"key":"5_CR30","doi-asserted-by":"crossref","unstructured":"Timmer, M., Katoen, J.-P., van de Pol, J.C., Stoelinga, M.I.A.: Efficient modelling and generation of Markov automata (extended version). Technical Report TR-CTIT-12-16, CTIT, University of Twente (2012)","DOI":"10.1007\/978-3-642-32940-1_26"},{"key":"5_CR31","series-title":"LNCS","first-page":"240","volume-title":"FORMATS 2013","author":"M. Timmer","year":"2013","unstructured":"Timmer, M., van de Pol, J.C., Stoelinga, M.I.A.: Confluence reduction for markov automata. In: Braberman, V., Fribourg, L. (eds.) FORMATS 2013. LNCS, vol.\u00a08053, pp. 240\u2013254. Springer, Heidelberg (2013)"},{"key":"5_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-642-04761-9_5","volume-title":"Automated Technology for Verification and Analysis","author":"J.C. Pol van de","year":"2009","unstructured":"van de Pol, J.C., Timmer, M.: State space reduction of linear processes using control flow reconstruction. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol.\u00a05799, pp. 54\u201368. Springer, Heidelberg (2009)"},{"key":"5_CR33","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.) TACAS 2010. LNCS, vol.\u00a06015, pp. 53\u201368. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Quantitative Evaluation of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40196-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T02:52:47Z","timestamp":1557975167000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40196-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642401954","9783642401961"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40196-1_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}