{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:48:58Z","timestamp":1740098938238,"version":"3.37.3"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319694825"},{"type":"electronic","value":"9783319694832"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-69483-2_2","type":"book-chapter","created":{"date-parts":[[2017,10,16]],"date-time":"2017-10-16T11:34:48Z","timestamp":1508153688000},"page":"25-41","source":"Crossref","is-referenced-by-count":3,"title":["Polynomial-Time Alternating Probabilistic Bisimulation for Interval MDPs"],"prefix":"10.1007","author":[{"given":"Vahid","family":"Hashemi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Turrini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ernst Moritz","family":"Hahn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Khaled","family":"Elbassioni","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,10,17]]},"reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/BFb0055622","volume-title":"CONCUR\u201998 Concurrency Theory","author":"R Alur","year":"1998","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 163\u2013178. Springer, Heidelberg (1998). doi: 10.1007\/BFb0055622"},{"key":"2_CR2","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":"2_CR3","doi-asserted-by":"crossref","unstructured":"Ben-Or, M.: Another advantage of free choice: completely asynchronous agreement protocols (extended abstract). In: PODC, pp. 27\u201330 (1983)","DOI":"10.1145\/800221.806707"},{"key":"2_CR4","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. LNCS, vol. 7795, pp. 32\u201346. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-36742-7_3"},{"issue":"2","key":"2_CR5","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. ITSE 35(2), 274\u2013292 (2009)","journal-title":"ITSE"},{"key":"2_CR6","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 \u2014 Concurrency Theory","author":"S Cattani","year":"2002","unstructured":"Cattani, S., Segala, R.: Decision algorithms for probabilistic bisimulation. In: Brim, L., K\u0159et\u00ednsk\u00fd, M., Ku\u010dera, A., Jan\u010dar, P. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 371\u2013386. Springer, Heidelberg (2002). doi: 10.1007\/3-540-45694-5_25"},{"key":"2_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 $$\\omega $$ -regular properties of interval Markov chains. In: Amadio, R. (ed.) FoSSaCS 2008. LNCS, vol. 4962, pp. 302\u2013317. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78499-9_22"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Chehaibar, G., Garavel, H., Mounier, L., Tawbi, N., Zulian, F.: Specification, verification of the PowerScale\u00ae bus arbitration protocol: An industrial experiment with LOTOS. In: FORTE, pp. 435\u2013450 (1996)","DOI":"10.1007\/978-0-387-35079-0_28"},{"key":"2_CR9","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. 5643, pp. 204\u2013218. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02658-4_18"},{"key":"2_CR10","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). doi: 10.1007\/978-3-642-18275-4_23"},{"key":"2_CR11","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":"2_CR12","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). doi: 10.1007\/978-3-642-21254-3_21"},{"key":"2_CR13","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 2006. LNCS, vol. 3925, pp. 71\u201388. Springer, Heidelberg (2006). doi: 10.1007\/11691617_5"},{"issue":"2","key":"2_CR14","doi-asserted-by":"crossref","first-page":"374","DOI":"10.1145\/3149.214121","volume":"32","author":"MJ Fischer","year":"1985","unstructured":"Fischer, M.J., Lynch, N.A., Paterson, M.S.: Impossibility of distributed consensus with one faulty process. J. ACM 32(2), 374\u2013382 (1985)","journal-title":"J. ACM"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-662-45489-3_5","volume-title":"Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems","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. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems. LNCS, vol. 8453, pp. 117\u2013155. Springer, Heidelberg (2014). doi: 10.1007\/978-3-662-45489-3_5"},{"issue":"1\u20132","key":"2_CR16","doi-asserted-by":"crossref","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":"2_CR17","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). doi: 10.1007\/978-3-642-20398-5_12"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-319-43425-4_4","volume-title":"Quantitative Evaluation of Systems","author":"EM Hahn","year":"2016","unstructured":"Hahn, E.M., Hashemi, V., Hermanns, H., Turrini, A.: Exploiting robust optimization for interval probabilistic bisimulation. In: Agha, G., Van Houdt, B. (eds.) QEST 2016. LNCS, vol. 9826, pp. 55\u201371. Springer, Cham (2016). doi: 10.1007\/978-3-319-43425-4_4"},{"issue":"5","key":"2_CR19","doi-asserted-by":"crossref","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":"2_CR20","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":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-319-30000-9_9","volume-title":"Language and Automata Theory and Applications","author":"V Hashemi","year":"2016","unstructured":"Hashemi, V., Hermanns, H., Song, L., Subramani, K., Turrini, A., Wojciechowski, P.: Compositional bisimulation minimization for interval Markov decision processes. In: Dediu, A.-H., Janou\u0161ek, J., Mart\u00edn-Vide, C., Truthe, B. (eds.) LATA 2016. LNCS, vol. 9618, pp. 114\u2013126. Springer, Cham (2016). doi: 10.1007\/978-3-319-30000-9_9"},{"key":"2_CR22","unstructured":"Hashemi, V., Hermanns, H., Turrini, A.: Compositional reasoning for interval Markov decision processes. http:\/\/arxiv.org\/abs\/1607.08484"},{"issue":"1","key":"2_CR23","first-page":"97","volume":"36","author":"H Hermanns","year":"2000","unstructured":"Hermanns, H., Katoen, J.-P.: Automated compositional Markov chain generation for a plain-old telephone system. SCP 36(1), 97\u2013127 (2000)","journal-title":"SCP"},{"issue":"2","key":"2_CR24","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1287\/moor.1040.0129","volume":"30","author":"GN Iyengar","year":"2005","unstructured":"Iyengar, G.N.: Robust dynamic programming. Math. Oper. Res. 30(2), 257\u2013280 (2005)","journal-title":"Math. Oper. Res."},{"key":"2_CR25","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":"2_CR26","doi-asserted-by":"crossref","unstructured":"Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. I&C, pp. 43\u201368 (1990)","DOI":"10.1016\/0890-5401(90)90025-D"},{"key":"2_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-71209-1_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J-P Katoen","year":"2007","unstructured":"Katoen, J.-P., Kemna, T., Zapreev, I., Jansen, D.N.: Bisimulation minimisation mostly speeds up probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 87\u2013101. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-71209-1_9"},{"issue":"2","key":"2_CR28","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1023\/A:1014745904458","volume":"8","author":"I Kozine","year":"2002","unstructured":"Kozine, I., Utkin, L.V.: Interval-valued finite Markov chains. Reliable Comput. 8(2), 97\u2013113 (2002)","journal-title":"Reliable Comput."},{"key":"2_CR29","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). doi: 10.1007\/978-3-642-22110-1_47"},{"issue":"8","key":"2_CR30","doi-asserted-by":"crossref","first-page":"2031","DOI":"10.1109\/TAC.2015.2398883","volume":"60","author":"M Lahijanian","year":"2015","unstructured":"Lahijanian, M., Andersson, S.B., Belta, C.: Formal verification and synthesis for discrete-time stochastic systems. IEEE Tr. Autom. Contr. 60(8), 2031\u20132045 (2015)","journal-title":"IEEE Tr. Autom. Contr."},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing (preliminary report). In: POPL, pp. 344\u2013352 (1989)","DOI":"10.1145\/75277.75307"},{"key":"2_CR32","series-title":"Springer Tracts in Advanced Robotics","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/978-3-319-16595-0_20","volume-title":"Algorithmic Foundations of Robotics XI","author":"R Luna","year":"2015","unstructured":"Luna, R., Lahijanian, M., Moll, M., Kavraki, L.E.: Asymptotically optimal stochastic motion planning with temporal goals. In: Akin, H.L., Amato, N.M., Isler, V., van der Stappen, A.F. (eds.) Algorithmic Foundations of Robotics XI. STAR, vol. 107, pp. 335\u2013352. Springer, Cham (2015). doi: 10.1007\/978-3-319-16595-0_20"},{"key":"2_CR33","doi-asserted-by":"crossref","unstructured":"Luna, R., Lahijanian, M., Moll, M., Kavraki, L.E.: Fast stochastic motion planning with optimality guarantees using local policy reconfiguration. In: ICRA, pp. 3013\u20133019 (2014)","DOI":"10.1109\/ICRA.2014.6907293"},{"key":"2_CR34","doi-asserted-by":"crossref","unstructured":"Luna, R., Lahijanian, M., Moll, M., Kavraki, L.E.: Optimal and efficient stochastic motion planning in partially-known environments. In: AAAI, pp. 2549\u20132555 (2014)","DOI":"10.1609\/aaai.v28i1.9054"},{"issue":"6","key":"2_CR35","doi-asserted-by":"crossref","first-page":"973","DOI":"10.1137\/0216062","volume":"16","author":"R Paige","year":"1987","unstructured":"Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973\u2013989 (1987)","journal-title":"SIAM J. Comput."},{"key":"2_CR36","unstructured":"PRISM model checker. http:\/\/www.prismmodelchecker.org\/"},{"key":"2_CR37","unstructured":"Puggelli, A.: Formal Techniques for the Verification and Optimal Control of Probabilistic Systems in the Presence of Modeling Uncertainties. Ph.D. thesis, EECS Department, University of California, Berkeley (2014)"},{"key":"2_CR38","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). doi: 10.1007\/978-3-642-39799-8_35"},{"key":"2_CR39","volume-title":"Theory of Linear and Integer Programming","author":"A Schrijver","year":"1998","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley, New York (1998)"},{"key":"2_CR40","unstructured":"Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. Ph.D. thesis, MIT (1995)"},{"key":"2_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/11817949_5","volume-title":"CONCUR 2006 \u2013 Concurrency Theory","author":"R Segala","year":"2006","unstructured":"Segala, R.: Probability and nondeterminism in operational models of concurrency. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 64\u201378. Springer, Heidelberg (2006). doi: 10.1007\/11817949_5"},{"key":"2_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/11691372_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Sen","year":"2006","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Model-checking markov chains in the presence of uncertainties. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 394\u2013410. Springer, Heidelberg (2006). doi: 10.1007\/11691372_26"},{"key":"2_CR43","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 (2012)","DOI":"10.1109\/CDC.2012.6426174"}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering. Theories, Tools, and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-69483-2_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,4]],"date-time":"2022-08-04T18:01:12Z","timestamp":1659636072000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-69483-2_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319694825","9783319694832"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-69483-2_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}