{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T06:11:49Z","timestamp":1725862309305},"publisher-location":"Cham","reference-count":47,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319434247"},{"type":"electronic","value":"9783319434254"}],"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-43425-4_4","type":"book-chapter","created":{"date-parts":[[2016,8,2]],"date-time":"2016-08-02T11:24:52Z","timestamp":1470137092000},"page":"55-71","source":"Crossref","is-referenced-by-count":5,"title":["Exploiting Robust Optimization for Interval Probabilistic Bisimulation"],"prefix":"10.1007","author":[{"given":"Ernst Moritz","family":"Hahn","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vahid","family":"Hashemi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Turrini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,8,3]]},"reference":[{"key":"4_CR1","unstructured":"Gurobi 4.0.2. http:\/\/www.gurobi.com\/"},{"key":"4_CR2","unstructured":"IBM ILOG CPLEX Optimizer. http:\/\/www.ibm.com\/software\/commerce\/optimization\/cplex-optimizer\/"},{"key":"4_CR3","unstructured":"PICOS: A Python interface for conic optimization solvers. http:\/\/picos.zib.de\/"},{"key":"4_CR4","unstructured":"PRISM model checker. http:\/\/www.prismmodelchecker.org\/"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Abate, A., El Ghaoui, L.: Robust model predictive control through adjustable variables: an application to path planning. In: CDC, pp. 2485\u20132490 (2004)","DOI":"10.1109\/CDC.2004.1428786"},{"key":"4_CR6","doi-asserted-by":"crossref","DOI":"10.1515\/9781400831050","volume-title":"Robust Optimization","author":"A Ben-Tal","year":"2009","unstructured":"Ben-Tal, A., El Ghaoui, L., Nemirovski, A.: Robust Optimization. Princeton University Press, Princeton (2009)"},{"issue":"2","key":"4_CR7","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1007\/s10107-003-0454-y","volume":"99","author":"A Ben-Tal","year":"2004","unstructured":"Ben-Tal, A., Goryashko, A., Guslitzer, E., Nemirovski, A.: Adjustable robust solutions of uncertain linear programs. Math. Program. 99(2), 351\u2013376 (2004)","journal-title":"Math. Program."},{"key":"4_CR8","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0167-6377(99)00016-4","volume":"25","author":"A Ben-Tal","year":"1999","unstructured":"Ben-Tal, A., Nemirovski, A.: Robust solutions of uncertain linear programs. Oper. Res. Lett. 25, 1\u201313 (1999)","journal-title":"Oper. Res. Lett."},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"issue":"3","key":"4_CR10","doi-asserted-by":"crossref","first-page":"464","DOI":"10.1137\/080734510","volume":"53","author":"D Bertsimas","year":"2011","unstructured":"Bertsimas, D., Brown, D.B., Caramanis, C.: Theory and applications of robust optimization. SIAM Rev. 53(3), 464\u2013501 (2011)","journal-title":"SIAM Rev."},{"key":"4_CR11","volume-title":"Probability and Measure","author":"P Billingsley","year":"1979","unstructured":"Billingsley, P.: Probability and Measure. Wiley, New York (1979)"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"issue":"7","key":"4_CR15","doi-asserted-by":"crossref","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":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"4_CR17","unstructured":"Dantzig, G.B., Madansky, A.: On the solution of two-stage linear programs under uncertainty. In: Proceedings of the Fourth Berkeley Symposium on Mathematical Statistics and Probability, vol. 1. pp. 165\u2013176 (1961)"},{"key":"4_CR18","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":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"4_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"issue":"1","key":"4_CR21","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/s00165-016-0356-4","volume":"28","author":"LM Ferrer Fioriti","year":"2016","unstructured":"Ferrer Fioriti, L.M., Hashemi, V., Hermanns, H., Turrini, A.: Deciding probabilistic automata weak bisimulation: theory and practice. Form. Asp. Comput. 28(1), 109\u2013143 (2016)","journal-title":"Form. Asp. Comput."},{"key":"4_CR22","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":"4_CR23","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."},{"issue":"6","key":"4_CR24","doi-asserted-by":"crossref","first-page":"1261","DOI":"10.1080\/10556788.2013.869807","volume":"29","author":"M Goerigk","year":"2014","unstructured":"Goerigk, M.: ROPI-a robust optimization programming interface for C++. Optim. Methods Softw. 29(6), 1261\u20131280 (2014)","journal-title":"Optim. Methods Softw."},{"issue":"2","key":"4_CR25","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/BF02579273","volume":"1","author":"M Gr\u00f6tschel","year":"1981","unstructured":"Gr\u00f6tschel, M., Lov\u00e1sz, L., Schrijver, A.: The ellipsoid method and its consequences in combinatorial optimization. Combinatorica 1(2), 169\u2013197 (1981)","journal-title":"Combinatorica"},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"4_CR27","doi-asserted-by":"crossref","unstructured":"Hashemi, V., Hatefi, H., Kr\u010d\u00e1l, J.: Probabilistic bisimulations for PCTL model checking of interval MDPs (extended version). In: SynCoP. EPTCS, vol. 145, pp. 19\u201333 (2014)","DOI":"10.4204\/EPTCS.145.4"},{"key":"4_CR28","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, Heidelberg (2016). doi: 10.1007\/978-3-319-30000-9_9"},{"issue":"1","key":"4_CR29","doi-asserted-by":"crossref","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. Comput. Program. 36(1), 97\u2013127 (2000)","journal-title":"Sci. Comput. Program."},{"issue":"2","key":"4_CR30","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":"4_CR31","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"},{"issue":"1","key":"4_CR32","doi-asserted-by":"crossref","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."},{"issue":"4","key":"4_CR33","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1007\/BF02579150","volume":"4","author":"N Karmarkar","year":"1984","unstructured":"Karmarkar, N.: A new polynomial-time algorithm for linear programming. Combinatorica 4(4), 373\u2013395 (1984)","journal-title":"Combinatorica"},{"issue":"1","key":"4_CR34","first-page":"191","volume":"20","author":"LG Khachyan","year":"1979","unstructured":"Khachyan, L.G.: A polynomial algorithm in linear programming. Sov. Math. Doklady 20(1), 191\u2013194 (1979)","journal-title":"Sov. Math. Doklady"},{"issue":"2","key":"4_CR35","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":"4_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"1","key":"4_CR37","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1080\/10556788.2010.517532","volume":"17","author":"J L\u00f6fberg","year":"2012","unstructured":"L\u00f6fberg, J.: Automatic robust convex programming. Optim. Methods Softw. 17(1), 115\u2013129 (2012)","journal-title":"Optim. Methods Softw."},{"issue":"5","key":"4_CR38","doi-asserted-by":"crossref","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."},{"issue":"6","key":"4_CR39","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":"4_CR40","unstructured":"Puggelli, A.: Formal techniques for the verification and optimal control of probabilistic systems in the presence of modeling uncertainties. Ph.D. thesis, University of California, Berkeley (2014)"},{"key":"4_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"4_CR42","unstructured":"Segala, R.: Modeling and verification of randomized distributed real-time systems. Ph.D. thesis, MIT (1995)"},{"key":"4_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"4_CR44","doi-asserted-by":"crossref","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":"4_CR45","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"},{"issue":"8\u20139","key":"4_CR46","doi-asserted-by":"crossref","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 bounded-parameter Markov decision processes. Artif. Intell. 172(8\u20139), 945\u2013954 (2008)","journal-title":"Artif. Intell."},{"key":"4_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS, vol. 863, pp. 680\u2013693. Springer, Heidelberg (1994)"}],"container-title":["Lecture Notes in Computer Science","Quantitative Evaluation of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-43425-4_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,11]],"date-time":"2019-09-11T22:15:42Z","timestamp":1568240142000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-43425-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319434247","9783319434254"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-43425-4_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}