{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T20:57:33Z","timestamp":1725742653025},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642401831"},{"type":"electronic","value":"9783642401848"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40184-8_26","type":"book-chapter","created":{"date-parts":[[2013,7,22]],"date-time":"2013-07-22T21:50:56Z","timestamp":1374529856000},"page":"364-379","source":"Crossref","is-referenced-by-count":6,"title":["Compositional Verification and Optimization of Interactive Markov Chains"],"prefix":"10.1007","author":[{"given":"Holger","family":"Hermanns","sequence":"first","affiliation":[]},{"given":"Jan","family":"Kr\u010d\u00e1l","sequence":"additional","affiliation":[]},{"given":"Jan","family":"K\u0159et\u00ednsk\u00fd","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","unstructured":"Alur, R., Henzinger, T.A.: Reactive modules. In: LICS, pp. 207\u2013218 (1996)"},{"key":"26_CR2","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, Part II. LNCS, vol.\u00a05556, pp. 103\u2013114. Springer, Heidelberg (2009)"},{"key":"26_CR3","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)"},{"issue":"1","key":"26_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(1), 2\u201326 (2005)","journal-title":"Theor. Comp. Sci."},{"key":"26_CR5","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1016\/j.cor.2010.08.011","volume":"38","author":"P. Buchholz","year":"2011","unstructured":"Buchholz, P., Schulz, I.: Numerical Analysis of Continuous Time Markov Decision processes over Finite Horizons. Computers and Operations Research\u00a038, 651\u2013659 (2011)","journal-title":"Computers and Operations Research"},{"key":"26_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-16242-8_1","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K. Chatterjee","year":"2010","unstructured":"Chatterjee, K., Doyen, L.: The complexity of partial-observation parity games. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol.\u00a06397, pp. 1\u201314. Springer, Heidelberg (2010)"},{"issue":"6","key":"26_CR7","doi-asserted-by":"publisher","first-page":"703","DOI":"10.1007\/s10009-012-0237-y","volume":"14","author":"A. David","year":"2012","unstructured":"David, A., Larsen, K.G., Legay, A., M\u00f8ller, M.H., Nyman, U., Ravn, A.P., Skou, A., Wasowski, A.: Compositional verification of real-time systems using ECDAR. STTT\u00a014(6), 703\u2013720 (2012)","journal-title":"STTT"},{"key":"26_CR8","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: Proc. of ICSE. ACM and IEEE Press (2012)","DOI":"10.1109\/ICSE.2012.6227118"},{"key":"26_CR9","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":"26_CR10","series-title":"LNCS","volume-title":"FSEN 2013","author":"H. Hatefi","year":"2013","unstructured":"Hatefi, H., Hermanns, H.: Improving time bounded reachability computations in interactive Markov chains. In: Arbab, F., Sirjani, M. (eds.) FSEN 2013. LNCS, vol.\u00a08161. Springer, Heidelberg (2013)"},{"key":"26_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-642-17071-3_16","volume-title":"Formal Methods for Components and Objects","author":"H. Hermanns","year":"2010","unstructured":"Hermanns, H., Katoen, J.-P.: The how and why of interactive Markov chains. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol.\u00a06286, pp. 311\u2013338. Springer, Heidelberg (2010)"},{"key":"26_CR12","doi-asserted-by":"crossref","unstructured":"Hermanns, H., Kr\u010d\u00e1l, J., K\u0159et\u00ednsk\u00fd, J.: Compositional verification and optimization of interactive markov chains. CoRR, abs\/1305.7332 (2013)","DOI":"10.1007\/978-3-642-40184-8_26"},{"key":"26_CR13","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: Proc. of DSN, pp. 419\u2013424 (2010)","DOI":"10.1109\/DSN.2010.5544290"},{"key":"26_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/3-540-45351-2_24","volume-title":"Hybrid Systems: Computation and Control","author":"T.A. Henzinger","year":"2001","unstructured":"Henzinger, T.A., Minea, M., Prabhu, V.S.: Assume-guarantee reasoning for hierarchical hybrid systems. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol.\u00a02034, pp. 275\u2013290. Springer, Heidelberg (2001)"},{"key":"26_CR15","doi-asserted-by":"crossref","unstructured":"Hahn, E.M., Norman, G., Parker, D., Wachter, B., Zhang, L.: Game-based abstraction and controller synthesis for probabilistic hybrid systems. In: QEST, pp. 69\u201378 (2011)","DOI":"10.1109\/QEST.2011.17"},{"key":"26_CR16","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":"26_CR17","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":"26_CR18","doi-asserted-by":"crossref","unstructured":"Koller, D., Megiddo, N., von Stengel, B.: Fast algorithms for finding randomized strategies in game trees. In: STOC, pp. 750\u2013759 (1994)","DOI":"10.1145\/195058.195451"},{"key":"26_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/3-540-61474-5_59","volume-title":"Computer Aided Verification","author":"O. Kupferman","year":"1996","unstructured":"Kupferman, O., Vardi, M.: Module checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 75\u201386. Springer, Heidelberg (1996)"},{"issue":"2","key":"26_CR20","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.peva.2010.04.001","volume":"68","author":"J.-P. Katoen","year":"2011","unstructured":"Katoen, J.-P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Performance Evaluation\u00a068(2), 90\u2013104 (2011)","journal-title":"Performance Evaluation"},{"key":"26_CR21","unstructured":"Larsen, K.G., Thomsen, B.: A modal process logic. In: LICS, pp. 203\u2013210 (1988)"},{"key":"26_CR22","doi-asserted-by":"crossref","unstructured":"Markovski, J.: Towards supervisory control of interactive Markov chains: Controllability. In: ACSD, pp. 108\u2013117 (2011)","DOI":"10.1109\/ACSD.2011.18"},{"issue":"4","key":"26_CR23","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1109\/TSE.1981.230844","volume":"7","author":"J. Misra","year":"1981","unstructured":"Misra, J., Mani Chandy, K.: Proofs of networks of processes. IEEE Trans. Software Eng.\u00a07(4), 417\u2013426 (1981)","journal-title":"IEEE Trans. Software Eng."},{"key":"26_CR24","doi-asserted-by":"crossref","unstructured":"Ramadge, P.J.G., Wonham, W.M.: The control of discrete event systems. Proceedings of the IEEE\u00a077(1) (1989)","DOI":"10.1109\/5.21072"},{"key":"26_CR25","doi-asserted-by":"crossref","unstructured":"Sproston, J.: Discrete-time verification and control for probabilistic rectangular hybrid automata. In: QEST, pp. 79\u201388 (2011)","DOI":"10.1109\/QEST.2011.18"},{"key":"26_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/3-540-61604-7_75","volume-title":"CONCUR \u201996: Concurrency Theory","author":"S. Tasiran","year":"1996","unstructured":"Tasiran, S., Alur, R., Kurshan, R.P., Brayton, R.K.: Verifying abstractions of timed systems. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol.\u00a01119, pp. 546\u2013562. Springer, Heidelberg (1996)"},{"key":"26_CR27","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","CONCUR 2013 \u2013 Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40184-8_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T01:42:37Z","timestamp":1557970957000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40184-8_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642401831","9783642401848"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40184-8_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}