{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T15:10:09Z","timestamp":1748790609457,"version":"3.41.0"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319299990"},{"type":"electronic","value":"9783319300009"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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-319-30000-9_9","type":"book-chapter","created":{"date-parts":[[2016,2,25]],"date-time":"2016-02-25T21:45:50Z","timestamp":1456436750000},"page":"114-126","source":"Crossref","is-referenced-by-count":7,"title":["Compositional Bisimulation Minimization for Interval Markov Decision Processes"],"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"}]},{"given":"K.","family":"Subramani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Turrini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Piotr","family":"Wojciechowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,2,26]]},"reference":[{"issue":"1","key":"9_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0166-218X(98)00136-X","volume":"89","author":"E Balas","year":"1998","unstructured":"Balas, E.: Disjunctive programming: properties of the convex hull of feasible points. Discrete Appl. Math. 89(1), 3\u201344 (1998)","journal-title":"Discrete Appl. Math."},{"key":"9_CR2","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":"9_CR3","volume-title":"Probability and Measure","author":"P Billingsley","year":"1979","unstructured":"Billingsley, P.: Probability and Measure. John Wiley and Sons, New York (1979)"},{"key":"9_CR4","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":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-540-31982-5_8","volume-title":"Foundations of Software Science and Computational Structures","author":"S Cattani","year":"2005","unstructured":"Cattani, S., Segala, R., Kwiatkowska, M., Norman, G.: Stochastic transition systems for continuous state spaces and non-determinism. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 125\u2013139. Springer, Heidelberg (2005)"},{"key":"9_CR6","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 $$ \u03c9 -regular properties of interval Markov chains. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 302\u2013317. Springer, Heidelberg (2008)"},{"doi-asserted-by":"crossref","unstructured":"Chehaibar, G., Garavel, H., Mounier, L., Tawbi, N., Zulian, F.: Specification and verification of the PowerScale $${}^{\\textregistered }$$ \u00ae busarbitration protocol: an industrial experiment with LOTOS. In: FORTE, pp. 435\u2013450 (1996)","key":"9_CR7","DOI":"10.1007\/978-0-387-35079-0_28"},{"issue":"7","key":"9_CR8","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":"9_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)"},{"key":"9_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)"},{"key":"9_CR11","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)"},{"issue":"4","key":"9_CR12","first-page":"301","volume":"71","author":"P Eirinakis","year":"2014","unstructured":"Eirinakis, P., Ruggieri, S., Subramani, K., Wojciechowski, P.: On quantified linear implications. AMAI 71(4), 301\u2013325 (2014)","journal-title":"AMAI"},{"key":"9_CR13","volume-title":"Computers and Intractability; A Guide to the Theory of NP-Completeness","author":"MR Garey","year":"1990","unstructured":"Garey, M.R., Johnson, D.S.: Computers and Intractability; A Guide to the Theory of NP-Completeness. W. H. Freeman & Co., New York (1990)"},{"key":"9_CR14","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)"},{"issue":"5","key":"9_CR15","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 Aspects Comput. 6(5), 512\u2013535 (1994)","journal-title":"Formal Aspects Comput."},{"key":"9_CR16","doi-asserted-by":"publisher","first-page":"19","DOI":"10.4204\/EPTCS.145.4","volume":"145","author":"V Hashemi","year":"2014","unstructured":"Hashemi, V., Hatefi, H., Kr\u010d\u00e1l, J.: Probabilistic bisimulations for PCTL model checking of interval MDPs. SynCoP EPTCS 145, 19\u201333 (2014)","journal-title":"SynCoP EPTCS"},{"unstructured":"Hashemi, V., Hermanns, H., Turrini, A.: On the efficiency of deciding probabilistic automata weak bisimulation. ECEASST, 66 (2013)","key":"9_CR17"},{"issue":"1","key":"9_CR18","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/S0167-6423(99)00019-2","volume":"36","author":"H Hermanns","year":"2000","unstructured":"Hermanns, H., Katoen, J.-P.: Automated compositional Markov chain generation for a plain-old telephone system. Sci. Comp. Progr. 36(1), 97\u2013127 (2000)","journal-title":"Sci. Comp. Progr."},{"issue":"4","key":"9_CR19","doi-asserted-by":"publisher","first-page":"941","DOI":"10.1287\/opre.2013.1172","volume":"61","author":"DA Iancu","year":"2013","unstructured":"Iancu, D.A., Sharma, M., Sviridenko, M.: Supermodularity and affine policies in dynamic robust optimization. Oper. Res. 61(4), 941\u2013956 (2013)","journal-title":"Oper. Res."},{"issue":"2","key":"9_CR20","doi-asserted-by":"publisher","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."},{"doi-asserted-by":"crossref","unstructured":"Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS, pp. 266\u2013277 (1991)","key":"9_CR21","DOI":"10.1109\/LICS.1991.151651"},{"issue":"1","key":"9_CR22","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/0890-5401(90)90025-D","volume":"86","author":"PC Kanellakis","year":"1990","unstructured":"Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput. 86(1), 43\u201368 (1990)","journal-title":"Inf. Comput."},{"key":"9_CR23","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)"},{"key":"9_CR24","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":"9_CR25","doi-asserted-by":"publisher","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":"9_CR26","volume-title":"Decision Procedures: An Algorithmic Point of View","author":"D Kroening","year":"2008","unstructured":"Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View, 1st edn. Springer, Heidelberg (2008)","edition":"1"},{"key":"9_CR27","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)"},{"issue":"5","key":"9_CR28","doi-asserted-by":"publisher","first-page":"780","DOI":"10.1287\/opre.1050.0216","volume":"53","author":"A Nilim","year":"2005","unstructured":"Nilim, A., Ghaoui, L.E.: Robust control of Markov decision processes with uncertain transition matrices. Oper. Res. 53(5), 780\u2013798 (2005)","journal-title":"Oper. Res."},{"issue":"6","key":"9_CR29","doi-asserted-by":"publisher","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":"9_CR30","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":"9_CR31","volume-title":"Theory of Linear and Integer Programming","author":"A Schrijver","year":"1998","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. John Wiley & Sons, Amsterdam (1998)"},{"unstructured":"Segala, R.: Modeling and verification of randomized distributed real-time systems. Ph.D. thesis, MIT (1995)","key":"9_CR32"},{"key":"9_CR33","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-asserted-by":"crossref","unstructured":"Subramani, K.: On the complexities of selected satisfiability and equivalence queries over boolean formulas and inclusion queries over hulls. JAMDS, 2009 (2009)","key":"9_CR34","DOI":"10.1155\/2009\/845804"},{"key":"9_CR35","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1016\/j.ic.2015.07.004","volume":"244","author":"A Turrini","year":"2015","unstructured":"Turrini, A., Hermanns, H.: Polynomial time decision algorithms for probabilistic automata. Inf. Comput. 244, 134\u2013171 (2015)","journal-title":"Inf. Comput."},{"key":"9_CR36","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/BF01580859","volume":"47","author":"PM Vaidya","year":"1990","unstructured":"Vaidya, P.M.: An algorithm for linear programming which requires $${O}(((m+n)n^2) + (m+n)^{1.5})n){L})$$ O ( ( ( m + n ) n 2 ) + ( m + n ) 1.5 ) n ) L ) arithmetic operations. Math. Program. 47, 175\u2013201 (1990)","journal-title":"Math. Program."},{"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)","key":"9_CR37","DOI":"10.1109\/CDC.2012.6426174"},{"issue":"8\u20139","key":"9_CR38","first-page":"945","volume":"172","author":"D Wu","year":"2008","unstructured":"Wu, D., Koutsoukos, X.D.: Reachability analysis of uncertain systems using bounded-parameter Markov decision processes. AI 172(8\u20139), 945\u2013954 (2008)","journal-title":"AI"},{"key":"9_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"680","DOI":"10.1007\/3-540-58468-4_190","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"W Yi","year":"1994","unstructured":"Yi, W.: Algebraic reasoning for real-time probabilistic processes with uncertain information. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863, pp. 680\u2013693. Springer, Heidelberg (1994)"}],"container-title":["Lecture Notes in Computer Science","Language and Automata Theory and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-30000-9_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T14:36:35Z","timestamp":1748788595000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-30000-9_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319299990","9783319300009"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-30000-9_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}