{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:12:49Z","timestamp":1778497969682,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642367410","type":"print"},{"value":"9783642367427","type":"electronic"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-36742-7_3","type":"book-chapter","created":{"date-parts":[[2013,2,18]],"date-time":"2013-02-18T19:41:56Z","timestamp":1361216516000},"page":"32-46","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":50,"title":["LTL Model Checking of Interval Markov Chains"],"prefix":"10.1007","author":[{"given":"Michael","family":"Benedikt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rastislav","family":"Lenhardt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"James","family":"Worrell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","first-page":"205","volume":"9","author":"N. Abe","year":"1992","unstructured":"Abe, N., Warmuth, M.K.: On the computational complexity of approximating distributions by probabilistic automata. Machine Learning\u00a09, 205\u2013260 (1992)","journal-title":"Machine Learning"},{"issue":"5","key":"3_CR2","doi-asserted-by":"publisher","first-page":"1987","DOI":"10.1137\/070697926","volume":"38","author":"E. Allender","year":"2009","unstructured":"Allender, E., B\u00fcrgisser, P., Kjeldgaard-Pedersen, J., Miltersen, P.B.: On the complexity of numerical analysis. SIAM J. Comput.\u00a038(5), 1987\u20132006 (2009)","journal-title":"SIAM J. Comput."},{"issue":"2","key":"3_CR3","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/0022-0000(86)90029-2","volume":"32","author":"M. Ben-Or","year":"1986","unstructured":"Ben-Or, M., Kozen, D., Reif, J.H.: The complexity of elementary algebra and geometry. JCSS\u00a032(2), 251\u2013264 (1986)","journal-title":"JCSS"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Blum, L., Cucker, F., Shub, M., Smale, S.: Complexity and real computation. Springer (1997)","DOI":"10.1007\/978-1-4612-0701-6"},{"issue":"1-3","key":"3_CR5","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/S0019-9958(83)80060-6","volume":"58","author":"A. Borodin","year":"1983","unstructured":"Borodin, A., Cook, S.A., Pippenger, N.: Parallel computation for well-endowed rings and space-bounded probabilistic machines. Information and Control\u00a058(1-3), 113\u2013136 (1983)","journal-title":"Information and Control"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Canny, J.F.: Some algebraic and geometric computations in pspace. In: STOC (1988)","DOI":"10.1145\/62212.62257"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/978-3-540-78499-9_22","volume-title":"Foundations of Software Science and Computational Structures","author":"K. Chatterjee","year":"2008","unstructured":"Chatterjee, K., Sen, K., Henzinger, T.A.: Model-Checking \u03c9-Regular Properties of Interval Markov Chains. In: Amadio, R. (ed.) FOSSACS 2008. LNCS, vol.\u00a04962, pp. 302\u2013317. Springer, Heidelberg (2008)"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-540-39813-4_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J.-M. Couvreur","year":"2003","unstructured":"Couvreur, J.-M., Saheb, N., Sutre, G.: An Optimal Automata Approach to LTL Model Checking of Probabilistic Systems. In: Vardi, M.Y., Voronkov, A. (eds.) LPAR 2003. LNCS, vol.\u00a02850, pp. 361\u2013375. Springer, Heidelberg (2003)"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-44804-7_3","volume-title":"Process Algebra and Probabilistic Methods. Performance Modelling and Verification","author":"P.R. D\u2019Argenio","year":"2001","unstructured":"D\u2019Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reachability Analysis of Probabilistic Systems by Successive Refinements. In: de Luca, L., Gilmore, S. (eds.) PAPM-PROBMIV 2001. LNCS, vol.\u00a02165, pp. 39\u201356. Springer, Heidelberg (2001)"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-642-21254-3_21","volume-title":"Language and Automata Theory and Applications","author":"B. Delahaye","year":"2011","unstructured":"Delahaye, B., Larsen, K.G., Legay, A., Pedersen, M.L., W\u0105sowski, A.: Decision Problems for Interval Markov Chains. In: Dediu, A.-H., Inenaga, S., Mart\u00edn-Vide, C. (eds.) LATA 2011. LNCS, vol.\u00a06638, pp. 274\u2013285. Springer, Heidelberg (2011)"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/11814764_12","volume-title":"Ad-Hoc, Mobile, and Wireless Networks","author":"A. Fehnker","year":"2006","unstructured":"Fehnker, A., Gao, P.: Formal Verification and Simulation for Performance Analysis for Probabilistic Broadcast Protocols. In: Kunz, T., Ravi, S.S. (eds.) ADHOC-NOW 2006. LNCS, vol.\u00a04104, pp. 128\u2013141. Springer, Heidelberg (2006)"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Protocol Specification Testing and Verification (1995)","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Gr\u00f6tschel, M., Lov\u00e1sz, L., Schrijver, A.: Geometric Algorithms and Combinatorial Optimization, vol.\u00a02. Springer (1993)","DOI":"10.1007\/978-3-642-78240-4"},{"key":"3_CR14","unstructured":"Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS (1991)"},{"issue":"2","key":"3_CR15","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1016\/j.tcs.2006.07.022","volume":"363","author":"J. Klein","year":"2006","unstructured":"Klein, J., Baier, C.: Experiments with deterministic \u03c9-automata for formulas of linear temporal logic. Theor. Comput. Sci.\u00a0363(2), 182\u2013195 (2006)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"3_CR16","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1287\/moor.12.3.441","volume":"12","author":"C. Papadimitriou","year":"1987","unstructured":"Papadimitriou, C., Tsitsiklis, J.N.: The complexity of markov decision processes. Math. Oper. Res.\u00a012(3), 441\u2013450 (1987)","journal-title":"Math. Oper. Res."},{"key":"3_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation\u00a0115, 1\u201337 (1994)","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-36742-7_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,1]],"date-time":"2020-06-01T00:04:11Z","timestamp":1590969851000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-36742-7_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642367410","9783642367427"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-36742-7_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]},"assertion":[{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}