{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,19]],"date-time":"2025-09-19T09:24:02Z","timestamp":1758273842804,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":41,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662491218"},{"type":"electronic","value":"9783662491225"}],"license":[{"start":{"date-parts":[[2015,12,25]],"date-time":"2015-12-25T00:00:00Z","timestamp":1451001600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49122-5_17","type":"book-chapter","created":{"date-parts":[[2015,12,24]],"date-time":"2015-12-24T05:01:36Z","timestamp":1450933296000},"page":"351-371","source":"Crossref","is-referenced-by-count":7,"title":["Reward-Bounded Reachability Probability for Uncertain Weighted MDPs"],"prefix":"10.1007","author":[{"given":"Vahid","family":"Hashemi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lei","family":"Song","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,12,25]]},"reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-40903-8_8","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"S Andova","year":"2004","unstructured":"Andova, S., Hermanns, H., Katoen, J.-P.: Discrete-time rewards model-checked. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791. Springer, Heidelberg (2004)"},{"issue":"3","key":"17_CR2","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1016\/0196-6774(90)90021-6","volume":"11","author":"J Aspnes","year":"1990","unstructured":"Aspnes, J., Herlihy, M.: Fast randomized consensus using shared memory. J. Algorithms 11(3), 441\u2013461 (1990)","journal-title":"J. Algorithms"},{"key":"17_CR3","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"key":"17_CR4","unstructured":"Baier, C., Gr\u00f6\u00dfer, M., Leucker, M., Bollig, B., Ciesinski, F.: Controller synthesis for probabilistic systems. In: Proceedings of IFIP TCS 2004. Kluwer (2004)"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-36742-7_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Benedikt","year":"2013","unstructured":"Benedikt, M., Lenhardt, R., Worrell, J.: LTL model checking of interval markov chains. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 32\u201346. Springer, Heidelberg (2013)"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"CONCUR 1996: Concurrency Theory","author":"M Bernardo","year":"1996","unstructured":"Bernardo, M., Gorrieri, R.: Extended markovian process algebra. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119. Springer, Heidelberg (1996)"},{"key":"17_CR7","volume-title":"Probability and Measure","author":"P Billingsley","year":"1979","unstructured":"Billingsley, P.: Probability and Measure. John Wiley and Sons, New York (1979)"},{"issue":"2","key":"17_CR8","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. ITSE 35(2), 274\u2013292 (2009)","journal-title":"ITSE"},{"issue":"2","key":"17_CR9","first-page":"128","volume":"7","author":"H Boudali","year":"2010","unstructured":"Boudali, H., Crouzen, P., Stoelinga, M.: A rigorous, compositional, and extensible framework for dynamic fault tree analysis. IEEE TDSC 7(2), 128\u2013143 (2010)","journal-title":"IEEE TDSC"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Bozga, M., David, A., Hartmanns, A., Hermanns, H., Larsen, K.G., Legay, A., Tretmans, J.: State-of-the-art tools and techniques for quantitative modeling and analysis of embedded systems. In: DATE, pp. 370\u2013375. IEEE, March 2012","DOI":"10.1109\/DATE.2012.6176499"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Cantino, A.S., Roberts, D.L., Isbell, C.L.: Autonomous nondeterministic tour guides: improving quality of experience with TTD-MDPs. In: AAMAS, p. 22. IFAAMAS (2007)","DOI":"10.1145\/1329125.1329152"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/3-540-45694-5_25","volume-title":"CONCUR 2002 - Concurrency Theory","author":"S Cattani","year":"2002","unstructured":"Cattani, S., Segala, R.: Decision algorithms for probabilistic bisimulation. In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Ku\u010dera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 371\u2013385. Springer, Heidelberg (2002)"},{"key":"17_CR13","doi-asserted-by":"crossref","first-page":"435","DOI":"10.1007\/978-0-387-35079-0_28","volume-title":"Formal Description Techniques IX","author":"Ghassan Chehaibar","year":"1996","unstructured":"Chehaibar, G., Garavel, H., Mounier, L., Tawbi, N., Zulian, F.: Specification and verification of the powerscale bus arbitration protocol: an industrial experiment with LOTOS. In: FORTE, pp. 435\u2013450 (1996)"},{"issue":"7","key":"17_CR14","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1016\/j.ipl.2013.01.004","volume":"113","author":"T Chen","year":"2013","unstructured":"Chen, T., Han, T., Kwiatkowska, M.: On the complexity of model checking interval-valued discrete time Markov chains. Inf. Process. Lett. 113(7), 210\u2013216 (2013)","journal-title":"Inf. Process. Lett."},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Delahaye, B., Katoen, J.-P., Larsen, K.G., Legay, A., Pedersen, M.L., Sher, F., Wasowski, A.: New results on abstract probabilistic automata. In: ACSD, pp. 118\u2013127 (2011)","DOI":"10.1109\/ACSD.2011.10"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/978-3-642-18275-4_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B Delahaye","year":"2011","unstructured":"Delahaye, B., Katoen, J.-P., Larsen, K.G., Legay, A., Pedersen, M.L., Sher, F., W\u0105sowski, A.: Abstract probabilistic automata. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 324\u2013339. Springer, Heidelberg (2011)"},{"key":"17_CR17","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. 6638, pp. 274\u2013285. Springer, Heidelberg (2011)"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/11691617_5","volume-title":"Model Checking Software","author":"H Fecher","year":"2006","unstructured":"Fecher, H., Leucker, M., Wolf, V.: Don\u2019t know in probabilistic systems. In: Valmari, A. (ed.) SPIN. LNCS, vol. 3925, pp. 71\u201388. Springer, Heidelberg (2006)"},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/978-3-662-45489-3_5","volume-title":"Stochastic Model Checking","author":"D Gebler","year":"2014","unstructured":"Gebler, D., Hashemi, V., Turrini, A.: Computing behavioral relations for probabilistic concurrent systems. In: Remke, A., Stoelinga, M. (eds.) Stochastic Model Checking. LNCS, vol. 8453, pp. 117\u2013155. Springer, Heidelberg (2014)"},{"issue":"1\u20132","key":"17_CR20","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/S0004-3702(00)00047-3","volume":"122","author":"R Givan","year":"2000","unstructured":"Givan, R., Leach, S.M., Dean, T.L.: Bounded-parameter markov decision processes. Artif. Intell. 122(1\u20132), 71\u2013109 (2000)","journal-title":"Artif. Intell."},{"key":"17_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-20398-5_12","volume-title":"NASA Formal Methods","author":"EM Hahn","year":"2011","unstructured":"Hahn, E.M., Han, T., Zhang, L.: Synthesis for PCTL in parametric markov decision processes. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 146\u2013161. Springer, Heidelberg (2011)"},{"key":"17_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-319-06410-9_22","volume-title":"FM 2014: Formal Methods","author":"EM Hahn","year":"2014","unstructured":"Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: iscasMc: a web-based probabilistic model checker. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 312\u2013317. Springer, Heidelberg (2014)"},{"issue":"5","key":"17_CR23","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Asp. Comput. 6(5), 512\u2013535 (1994)","journal-title":"Formal Asp. Comput."},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Hashemi, V., Hatefi, H., Kr\u010d\u00e1l, J.: Probabilistic bisimulations for PCTL model checking of interval mdps. In: SynCoP, pp. 19\u201333. EPTCS (2014)","DOI":"10.4204\/EPTCS.145.4"},{"key":"17_CR25","unstructured":"Hashemi, V., Hermanss, H., Turrini, A.: On the efficiency of deciding probabilistic automata weak bisimulation. Electron. Commun. EASST, vol. 66 (2013)"},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS, pp. 266\u2013277 (1991)","DOI":"10.1109\/LICS.1991.151651"},{"key":"17_CR27","first-page":"43","volume":"86","author":"PC Kanellakis","year":"1990","unstructured":"Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. I&C 86, 43\u201368 (1990)","journal-title":"I&C"},{"key":"17_CR28","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. 5813, pp. 195\u2013211. Springer, Heidelberg (2009)"},{"issue":"2","key":"17_CR29","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1023\/A:1014745904458","volume":"8","author":"IO Kozine","year":"2011","unstructured":"Kozine, I.O., Utkin, L.V.: Interval-valued finite markov chains. Reliable Comput. 8(2), 97\u2013113 (2011)","journal-title":"Reliable Comput."},{"key":"17_CR30","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 $$\\omega $$ -regular properties of interval markov chains. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 302\u2013317. Springer, Heidelberg (2008)"},{"key":"17_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"17_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/3-540-44585-4_17","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2001","unstructured":"Kwiatkowska, M., Norman, G., Segala, R.: Automated verification of a randomized distributed consensus protocol using cadence SMV and PRISM. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 194\u2013206. Springer, Heidelberg (2001)"},{"key":"17_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-540-45187-7_14","volume-title":"CONCUR 2003 - Concurrency Theory","author":"NA Lynch","year":"2003","unstructured":"Lynch, N.A., Segala, R., Vaandrager, F.W.: Compositionality for probabilistic automata. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 208\u2013221. Springer, Heidelberg (2003)"},{"issue":"2","key":"17_CR34","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1145\/190.191","volume":"2","author":"MA Marsan","year":"1984","unstructured":"Marsan, M.A., Conte, G., Balbo, G.: A class of generalized stochastic Petri nets for the performance evaluation of multiprocessor systems. ACM Trans. Comput. Syst. 2(2), 93\u2013122 (1984)","journal-title":"ACM Trans. Comput. Syst."},{"issue":"5","key":"17_CR35","doi-asserted-by":"publisher","first-page":"780","DOI":"10.1287\/opre.1050.0216","volume":"53","author":"A Nilim","year":"2005","unstructured":"Nilim, A., El Ghaoui, L.: Robust control of Markov decision processes with uncertain transition matrices. Oper. Res. 53(5), 780\u2013798 (2005)","journal-title":"Oper. Res."},{"key":"17_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-642-39799-8_35","volume-title":"Computer Aided Verification","author":"A Puggelli","year":"2013","unstructured":"Puggelli, A., Li, W., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Polynomial-time verification of PCTL properties of MDPs with convex uncertainties. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 527\u2013542. Springer, Heidelberg (2013)"},{"key":"17_CR37","series-title":"Probability and Statistics","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"ML Puterman","year":"2005","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Probability and Statistics, vol. 594. John Wiley & Sons Inc., New York (2005)"},{"key":"17_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-44667-2_6","volume-title":"Lectures on Formal Methods and Performance Analysis","author":"R Segala","year":"2001","unstructured":"Segala, R.: Verification of randomized distributed algorithms. In: Brinksma, E., Hermanns, H., Katoen, J.-P. (eds.) EEF School 2000 and FMPA 2000. LNCS, vol. 2090, pp. 232\u2013260. Springer, Heidelberg (2001)"},{"issue":"2","key":"17_CR39","first-page":"250","volume":"2","author":"R Segala","year":"1995","unstructured":"Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. Nord. J. Comput. 2(2), 250\u2013273 (1995)","journal-title":"Nord. J. Comput."},{"key":"17_CR40","doi-asserted-by":"crossref","unstructured":"Wolff, E.M., Topcu, U., Murray, R.M.: Robust control of uncertain markov decision processes with temporal logic specifications. In: CDC, pp. 3372\u20133379. IEEE (2012)","DOI":"10.1109\/CDC.2012.6426174"},{"issue":"8\u20139","key":"17_CR41","doi-asserted-by":"publisher","first-page":"945","DOI":"10.1016\/j.artint.2007.12.002","volume":"172","author":"D Wu","year":"2008","unstructured":"Wu, D., Koutsoukos, X.D.: Reachability analysis of uncertain systems using boundedparameter markov decision processes. Artif. Intell. 172(8\u20139), 945\u2013954 (2008)","journal-title":"Artif. Intell."}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49122-5_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T22:49:42Z","timestamp":1748731782000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49122-5_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12,25]]},"ISBN":["9783662491218","9783662491225"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49122-5_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015,12,25]]}}}