{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T03:14:42Z","timestamp":1776482082841,"version":"3.51.2"},"publisher-location":"Cham","reference-count":154,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319919072","type":"print"},{"value":"9783319919089","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-319-91908-9_21","type":"book-chapter","created":{"date-parts":[[2019,10,4]],"date-time":"2019-10-04T05:05:00Z","timestamp":1570165500000},"page":"420-451","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":19,"title":["The 10,000 Facets of MDP Model Checking"],"prefix":"10.1007","author":[{"given":"Christel","family":"Baier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,10,5]]},"reference":[{"issue":"2","key":"21_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"21_CR2","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/978-3-319-91908-9_22","volume-title":"Computing and Software Science","author":"R Alur","year":"2018","unstructured":"Alur, R., Giacobbe, M., Henzinger, T., Larsen, K., Mikucionis, M.: Continuous-time models for system design and analysis. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 452\u2013477. Springer, Cham (2018)"},{"issue":"28","key":"21_CR3","doi-asserted-by":"publisher","first-page":"3072","DOI":"10.1016\/j.tcs.2011.02.045","volume":"412","author":"ME Andr\u00e9s","year":"2011","unstructured":"Andr\u00e9s, M.E., Palamidessi, C., van Rossum, P., Sokolova, A.: Information hiding in probabilistic concurrent systems. Theor. Comput. Sci. 412(28), 3072\u20133089 (2011)","journal-title":"Theor. Comput. Sci."},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-540-78800-3_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"ME Andr\u00e9s","year":"2008","unstructured":"Andr\u00e9s, M.E., van Rossum, P.: Conditional probabilities over probabilistic and nondeterministic systems. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 157\u2013172. Springer, Heidelberg (2008). \n                      https:\/\/doi.org\/10.1007\/978-3-540-78800-3_12"},{"issue":"2\/3","key":"21_CR5","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1023\/A:1008699807402","volume":"10","author":"IR Bahar","year":"1997","unstructured":"Bahar, I.R., Frohm, E.A., Gaona, C.M., Hachtel, G.D., Macii, E., Pardo, A., Somenzi, F.: Algebraic decision diagrams and their applications. Form. Methods Syst. Des. 10(2\/3), 171\u2013206 (1997)","journal-title":"Form. Methods Syst. Des."},{"key":"21_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-540-78499-9_21","volume-title":"Foundations of Software Science and Computational Structures","author":"C Baier","year":"2008","unstructured":"Baier, C., Bertrand, N., Gr\u00f6\u00dfer, M.: On decision problems for probabilistic B\u00fcchi automata. In: Amadio, R. (ed.) FoSSaCS 2008. LNCS, vol. 4962, pp. 287\u2013301. Springer, Heidelberg (2008). \n                      https:\/\/doi.org\/10.1007\/978-3-540-78499-9_21"},{"issue":"1","key":"21_CR7","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/1297658.1297663","volume":"9","author":"C Baier","year":"2007","unstructured":"Baier, C., Bertrand, N., Schnoebelen, P.: Verifying nondeterministic probabilistic channel systems against \n                      \n                        \n                      \n                      $$\\omega $$\n                    -regular linear-time properties. ACM Trans. Comput. Log. 9(1), 5 (2007)","journal-title":"ACM Trans. Comput. Log."},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/3-540-63165-8_199","volume-title":"Automata, Languages and Programming","author":"C Baier","year":"1997","unstructured":"Baier, C., Clarke, E.M., Hartonas-Garmhausen, V., Kwiatkowska, M., Ryan, M.: Symbolic model checking for probabilistic processes. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, pp. 430\u2013440. Springer, Heidelberg (1997). \n                      https:\/\/doi.org\/10.1007\/3-540-63165-8_199"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/978-3-319-06200-6_24","volume-title":"NASA Formal Methods","author":"C Baier","year":"2014","unstructured":"Baier, C., Daum, M., Dubslaff, C., Klein, J., Kl\u00fcppelholz, S.: Energy-utility quantiles. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 285\u2013299. Springer, Cham (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-319-06200-6_24"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Baier, C., Dubslaff, C., Kl\u00fcppelholz, S.: Trade-off analysis meets probabilistic model checking. In: CSL-LICS, pp. 1:1\u20131:10. ACM (2014)","DOI":"10.1145\/2603088.2603089"},{"issue":"1","key":"21_CR11","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1006\/jcss.1999.1683","volume":"60","author":"C Baier","year":"2000","unstructured":"Baier, C., Engelen, B., Majster-Cederbaum, M.E.: Deciding bisimilarity and similarity for probabilistic processes. J. Comput. Syst. Sci. 60(1), 187\u2013231 (2000)","journal-title":"J. Comput. Syst. Sci."},{"issue":"1","key":"21_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2108242.2108243","volume":"59","author":"C Baier","year":"2012","unstructured":"Baier, C., Gr\u00f6\u00dfer, M., Bertrand, N.: Probabilistic \n                      \n                        \n                      \n                      $$\\omega $$\n                    -automata. J. ACM 59(1), 1 (2012)","journal-title":"J. ACM"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"Baier, C., Gr\u00f6\u00dfer, M., Ciesinski, F.: Partial order reduction for probabilistic systems. In: QEST, pp. 230\u2013239. IEEE Computer Society (2004)","DOI":"10.1109\/QEST.2004.1348037"},{"key":"21_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-04761-9_12","volume-title":"Automated Technology for Verification and Analysis","author":"C Baier","year":"2009","unstructured":"Baier, C., Groesser, M., Ciesinski, F.: Quantitative analysis under fairness constraints. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 135\u2013150. Springer, Heidelberg (2009). \n                      https:\/\/doi.org\/10.1007\/978-3-642-04761-9_12"},{"key":"21_CR15","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Reachability in continuous-time Markov reward decision processes. In: Logic and Automata History and Perspectives. Texts in Logic and Games, vol. 2, pp. 53\u201372. Amsterdam University Press (2008)"},{"issue":"1","key":"21_CR16","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2005.07.022","volume":"345","author":"C Baier","year":"2005","unstructured":"Baier, C., Hermanns, H., Katoen, J.-P., Haverkort, B.R.: Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Theoret. Comput. Sci. 345(1), 2\u201326 (2005)","journal-title":"Theoret. Comput. Sci."},{"key":"21_CR17","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":"21_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-642-54862-8_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Baier","year":"2014","unstructured":"Baier, C., Klein, J., Kl\u00fcppelholz, S., M\u00e4rcker, S.: Computing conditional probabilities in markovian models efficiently. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 515\u2013530. Springer, Heidelberg (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-642-54862-8_43"},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Baier, C., Klein, J., Kl\u00fcppelholz, S., Wunderlich, S.: Weight monitoring with linear temporal logic: complexity and decidability. In: CSL-LICS, pp. 11:1\u201311:10. ACM (2014)","DOI":"10.1145\/2603088.2603162"},{"key":"21_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-662-54580-5_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Baier","year":"2017","unstructured":"Baier, C., Klein, J., Kl\u00fcppelholz, S., Wunderlich, S.: Maximizing the conditional expected reward for reaching the goal. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 269\u2013285. Springer, Heidelberg (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-662-54580-5_16"},{"issue":"3","key":"21_CR21","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/s004460050046","volume":"11","author":"C Baier","year":"1998","unstructured":"Baier, C., Kwiatkowska, M.Z.: Model checking for a probabilistic branching time logic with fairness. Distrib. Comput. 11(3), 125\u2013155 (1998)","journal-title":"Distrib. Comput."},{"key":"21_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-319-43425-4_17","volume-title":"Quantitative Evaluation of Systems","author":"E Bartocci","year":"2016","unstructured":"Bartocci, E., Bortolussi, L., Br\u00e1zdil, T., Milios, D., Sanguinetti, G.: Policy learning for time-bounded reachability in continuous-time Markov decision processes via doubly-stochastic gradient ascent. In: Agha, G., Van Houdt, B. (eds.) QEST 2016. LNCS, vol. 9826, pp. 244\u2013259. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-43425-4_17"},{"key":"21_CR23","first-page":"679","volume":"38","author":"R Bellman","year":"1957","unstructured":"Bellman, R.: A Markovian decision process. J. Math. Mech. 38, 679\u2013684 (1957)","journal-title":"J. Math. Mech."},{"key":"21_CR24","doi-asserted-by":"crossref","unstructured":"Ben-Or, M.: Another advantage of free choice: completely asynchronous agreement protocols (extended abstract). In: PODC, pp. 27\u201330. ACM (1983)","DOI":"10.1145\/800221.806707"},{"key":"21_CR25","doi-asserted-by":"crossref","unstructured":"Bertrand, N., Bouyer, P., Brihaye, T., Menet, Q., Baier, C., Gr\u00f6\u00dfer, M., Jurdzinski, M.: Stochastic timed automata. Log. Methods Comput. Sci. 10(4) (2014)","DOI":"10.2168\/LMCS-10(4:6)2014"},{"issue":"3","key":"21_CR26","doi-asserted-by":"publisher","first-page":"580","DOI":"10.1287\/moor.16.3.580","volume":"16","author":"DP Bertsekas","year":"1991","unstructured":"Bertsekas, D.P., Tsitsiklis, J.N.: An analysis of stochastic shortest path problems. Math. Oper. Res. 16(3), 580\u2013595 (1991)","journal-title":"Math. Oper. Res."},{"key":"21_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"A Bianco","year":"1995","unstructured":"Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499\u2013513. Springer, Heidelberg (1995). \n                      https:\/\/doi.org\/10.1007\/3-540-60692-0_70"},{"key":"21_CR28","doi-asserted-by":"publisher","first-page":"51","DOI":"10.4204\/EPTCS.157.8","volume":"157","author":"Aaron Bohy","year":"2014","unstructured":"Bohy, A., Bruy\u00e8re, V., Raskin, J.-F.: Symblicit algorithms for optimal strategy synthesis in monotonic Markov decision processes. In: SYNT. EPTCS, vol. 157, pp. 51\u201367 (2014)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"issue":"4","key":"21_CR29","doi-asserted-by":"publisher","first-page":"27:1","DOI":"10.1145\/2629686","volume":"15","author":"U Boker","year":"2014","unstructured":"Boker, U., Chatterjee, K., Henzinger, T.A., Kupferman, O.: Temporal specifications with accumulative values. ACM Trans. Comput. Log. 15(4), 27:1\u201327:25 (2014)","journal-title":"ACM Trans. Comput. Log."},{"issue":"1","key":"21_CR30","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s10009-010-0176-4","volume":"13","author":"D Bosnacki","year":"2011","unstructured":"Bosnacki, D., Edelkamp, S., Sulewski, D., Wijs, A.: Parallel probabilistic model checking on general purpose graphics processors. STTT 13(1), 21\u201335 (2011)","journal-title":"STTT"},{"key":"21_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/BFb0023733","volume-title":"Computer-Aided Verification","author":"A Bouajjani","year":"1991","unstructured":"Bouajjani, A., Fernandez, J.-C., Halbwachs, N.: Minimal model generation. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 197\u2013203. Springer, Heidelberg (1991). \n                      https:\/\/doi.org\/10.1007\/BFb0023733"},{"key":"21_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-85778-5_4","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"P Bouyer","year":"2008","unstructured":"Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Srba, J.: Infinite runs in weighted timed automata with energy constraints. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 33\u201347. Springer, Heidelberg (2008). \n                      https:\/\/doi.org\/10.1007\/978-3-540-85778-5_4"},{"key":"21_CR33","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Brozek, V., Chatterjee, K., Forejt, V., Kucera, A.: Markov decision processes with multiple long-run average objectives. Log. Methods Comput. Sci. 10(1) (2014)","DOI":"10.2168\/LMCS-10(1:13)2014"},{"key":"21_CR34","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Brozek, V., Chatterjee, K., Forejt, V., Kucera, A.: Two views on multiple mean-payoff objectives in Markov decision processes. Log. Methods Comput. Sci. 10(1) (2014)","DOI":"10.2168\/LMCS-10(1:13)2014"},{"key":"21_CR35","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/j.ic.2012.01.008","volume":"222","author":"T Br\u00e1zdil","year":"2013","unstructured":"Br\u00e1zdil, T., Brozek, V., Etessami, K., Kucera, A.: Approximating the termination value of one-counter MDPs and stochastic games. Inf. Comput. 222, 121\u2013138 (2013)","journal-title":"Inf. Comput."},{"key":"21_CR36","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Brozek, V., Etessami, K., Kucera, A., Wojtczak, D.: One-counter Markov decision processes. In: SODA, pp. 863\u2013874. SIAM (2010)","DOI":"10.1137\/1.9781611973075.70"},{"key":"21_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-319-11936-6_8","volume-title":"Automated Technology for Verification and Analysis","author":"T Br\u00e1zdil","year":"2014","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Chmel\u00edk, M., Forejt, V., K\u0159et\u00ednsk\u00fd, J., Kwiatkowska, M., Parker, D., Ujma, M.: Verification of Markov decision processes using learning algorithms. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 98\u2013114. Springer, Cham (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-319-11936-6_8"},{"key":"21_CR38","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1016\/j.jcss.2016.09.009","volume":"84","author":"T Br\u00e1zdil","year":"2017","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Forejt, V., Kucera, A.: Trading performance for stability in Markov decision processes. J. Comput. Syst. Sci. 84, 144\u2013170 (2017)","journal-title":"J. Comput. Syst. Sci."},{"key":"21_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-319-46520-3_3","volume-title":"Automated Technology for Verification and Analysis","author":"T Br\u00e1zdil","year":"2016","unstructured":"Br\u00e1zdil, T., Ku\u010dera, A., Novotn\u00fd, P.: Optimizing the expected mean payoff in energy Markov decision processes. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 32\u201349. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-46520-3_3"},{"issue":"1","key":"21_CR40","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1145\/322234.322242","volume":"28","author":"JL Bruno","year":"1981","unstructured":"Bruno, J.L., Downey, P.J., Frederickson, G.N.: Sequencing tasks with exponential service times to minimize the expected flow time or makespan. J. ACM 28(1), 100\u2013113 (1981)","journal-title":"J. ACM"},{"key":"21_CR41","unstructured":"Bruy\u00e8re, V., Filiot, E., Randour, M., Raskin, J.-F.: Meet your expectations with guarantees: beyond worst-case synthesis in quantitative games. In: STACS. LIPIcs, , vol. 25, pp. 199\u2013213. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2014)"},{"key":"21_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-642-22110-1_19","volume-title":"Computer Aided Verification","author":"P Buchholz","year":"2011","unstructured":"Buchholz, P., Hahn, E.M., Hermanns, H., Zhang, L.: Model checking algorithms for CTMDPs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 225\u2013242. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-22110-1_19"},{"issue":"2","key":"21_CR43","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: \n                      \n                        \n                      \n                      $$10^\\wedge 20$$\n                     states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"key":"21_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-319-24953-7_12","volume-title":"Automated Technology for Verification and Analysis","author":"Y Butkova","year":"2015","unstructured":"Butkova, Y., Hatefi, H., Hermanns, H., Kr\u010d\u00e1l, J.: Optimal continuous time Markov decisions. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 166\u2013182. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-24953-7_12"},{"issue":"1","key":"21_CR45","doi-asserted-by":"publisher","first-page":"1:1","DOI":"10.1145\/1838552.1838553","volume":"12","author":"R Chadha","year":"2010","unstructured":"Chadha, R., Viswanathan, M.: A counterexample-guided abstraction-refinement framework for Markov decision processes. ACM Trans. Comput. Log. 12(1), 1:1\u20131:49 (2010)","journal-title":"ACM Trans. Comput. Log."},{"key":"21_CR46","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1016\/j.artint.2016.01.007","volume":"234","author":"K Chatterjee","year":"2016","unstructured":"Chatterjee, K., Chmelik, M., Gupta, R., Kanodia, A.: Optimal cost almost-sure reachability in POMDPs. Artif. Intell. 234, 26\u201348 (2016)","journal-title":"Artif. Intell."},{"issue":"5","key":"21_CR47","doi-asserted-by":"publisher","first-page":"878","DOI":"10.1016\/j.jcss.2016.02.009","volume":"82","author":"K Chatterjee","year":"2016","unstructured":"Chatterjee, K., Chmelik, M., Tracol, M.: What is decidable about partially observable Markov decision processes with \n                      \n                        \n                      \n                      $$\\omega $$\n                    -regular objectives. J. Comput. Syst. Sci. 82(5), 878\u2013911 (2016)","journal-title":"J. Comput. Syst. Sci."},{"key":"21_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-642-22993-0_21","volume-title":"Mathematical Foundations of Computer Science 2011","author":"K Chatterjee","year":"2011","unstructured":"Chatterjee, K., Doyen, L.: Energy and mean-payoff parity Markov decision processes. In: Murlak, F., Sankowski, P. (eds.) MFCS 2011. LNCS, vol. 6907, pp. 206\u2013218. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-22993-0_21"},{"key":"21_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/11672142_26","volume-title":"STACS 2006","author":"K Chatterjee","year":"2006","unstructured":"Chatterjee, K., Majumdar, R., Henzinger, T.A.: Markov decision processes with multiple objectives. In: Durand, B., Thomas, W. (eds.) STACS 2006. LNCS, vol. 3884, pp. 325\u2013336. Springer, Heidelberg (2006). \n                      https:\/\/doi.org\/10.1007\/11672142_26"},{"issue":"4","key":"21_CR50","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857\u2013907 (1995)","journal-title":"J. ACM"},{"key":"21_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-662-54580-5_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Cubuktepe","year":"2017","unstructured":"Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.-P., Papusha, I., Poonawala, H.A., Topcu, U.: Sequential convex programming for the efficient verification of parametric MDPs. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 133\u2013150. Springer, Heidelberg (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-662-54580-5_8"},{"key":"21_CR52","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":"PR 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 Alfaro, L., Gilmore, S. (eds.) PAPM-PROBMIV 2001. LNCS, vol. 2165, pp. 39\u201356. Springer, Heidelberg (2001). \n                      https:\/\/doi.org\/10.1007\/3-540-44804-7_3"},{"key":"21_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/3-540-45605-8_5","volume-title":"Process Algebra and Probabilistic Methods: Performance Modeling and Verification","author":"PR D\u2019Argenio","year":"2002","unstructured":"D\u2019Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reduction and refinement strategies for probabilistic analysis. In: Hermanns, H., Segala, R. (eds.) PAPM-PROBMIV 2002. LNCS, vol. 2399, pp. 57\u201376. Springer, Heidelberg (2002). \n                      https:\/\/doi.org\/10.1007\/3-540-45605-8_5"},{"key":"21_CR54","doi-asserted-by":"crossref","unstructured":"D\u2019Argenio, P.R., Niebert, P.: Partial order reduction on concurrent probabilistic programs. In: QEST, pp. 240\u2013249. IEEE Computer Society (2004)","DOI":"10.1109\/QEST.2004.1348038"},{"issue":"4","key":"21_CR55","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B.: Uppaal SMC tutorial. STTT 17(4), 397\u2013415 (2015)","journal-title":"STTT"},{"key":"21_CR56","unstructured":"de Alfaro, L.: Formal verification of probabilistic systems. Ph.D. thesis, Department of Computer Science, Stanford University (1997)"},{"key":"21_CR57","unstructured":"de Alfaro, L.: How to specify and verify the long-run average behavior of probabilistic systems. In: LICS, pp. 454\u2013465. IEEE Computer Society (1998)"},{"key":"21_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/3-540-48320-9_7","volume-title":"CONCUR \u201999 Concurrency Theory","author":"L Alfaro de","year":"1999","unstructured":"de Alfaro, L.: Computing minimum and maximum reachability times in probabilistic systems. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 66\u201381. Springer, Heidelberg (1999). \n                      https:\/\/doi.org\/10.1007\/3-540-48320-9_7"},{"key":"21_CR59","unstructured":"de Alfaro, L.: The verification of probabilistic systems under memoryless partial-information policies is hard. In: Proceedings of 2nd International Workshop on Probabilistic Methods in Verification (ProbMiV 1999), Research Report CSR-99-9, pp. 19\u201332. Birmingham University (1999)"},{"key":"21_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/3-540-46419-0_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Alfaro de","year":"2000","unstructured":"de Alfaro, L., Kwiatkowska, M., Norman, G., Parker, D., Segala, R.: Symbolic model checking of probabilistic processes using MTBDDs and the Kronecker representation. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 395\u2013410. Springer, Heidelberg (2000). \n                      https:\/\/doi.org\/10.1007\/3-540-46419-0_27"},{"key":"21_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-540-73368-3_38","volume-title":"Computer Aided Verification","author":"L Alfaro de","year":"2007","unstructured":"de Alfaro, L., Roy, P.: Magnifying-lens abstraction for Markov decision processes. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 325\u2013338. Springer, Heidelberg (2007). \n                      https:\/\/doi.org\/10.1007\/978-3-540-73368-3_38"},{"key":"21_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-662-45489-3_4","volume-title":"Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems","author":"C Dehnert","year":"2014","unstructured":"Dehnert, C., Gebler, D., Volpato, M., Jansen, D.N.: On abstraction of probabilistic systems. In: Remke, A., Stoelinga, M. (eds.) ROCKS 2012. LNCS, vol. 8453, pp. 87\u2013116. Springer, Heidelberg (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-662-45489-3_4"},{"key":"21_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-319-63390-9_31","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2017","unstructured":"Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592\u2013600. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31"},{"key":"21_CR64","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1016\/j.ic.2013.10.002","volume":"232","author":"B Delahaye","year":"2013","unstructured":"Delahaye, B., Katoen, J.-P., Larsen, K.G., Legay, A., Pedersen, M.L., Sher, F., Wasowski, A.: Abstract probabilistic automata. Inf. Comput. 232, 66\u2013116 (2013)","journal-title":"Inf. Comput."},{"key":"21_CR65","doi-asserted-by":"crossref","unstructured":"Donaldson, A.F., Miller, A., Parker, D.: Language-level symmetry reduction for probabilistic model checking. In: QEST, pp. 289\u2013298. IEEE Computer Society (2009)","DOI":"10.1109\/QEST.2009.21"},{"key":"21_CR66","doi-asserted-by":"crossref","unstructured":"Dr\u00e4ger, K., Forejt, V., Kwiatkowska, M.Z., Parker, D., Ujma, M.: Permissive controller synthesis for probabilistic systems. Log. Methods Comput. Sci. 11(2) (2015)","DOI":"10.2168\/LMCS-11(2:16)2015"},{"key":"21_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-642-40196-1_6","volume-title":"Quantitative Evaluation of Systems","author":"C Eisentraut","year":"2013","unstructured":"Eisentraut, C., Hermanns, H., Kr\u00e4mer, J., Turrini, A., Zhang, L.: Deciding bisimilarities on distributions. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 72\u201388. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-40196-1_6"},{"key":"21_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-642-36742-7_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Eisentraut","year":"2013","unstructured":"Eisentraut, C., Hermanns, H., Schuster, J., Turrini, A., Zhang, L.: The quest for minimal quotients for probabilistic automata. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 16\u201331. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-36742-7_2"},{"key":"21_CR69","doi-asserted-by":"crossref","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: LICS, pp. 342\u2013351. IEEE CS (2010)","DOI":"10.1109\/LICS.2010.41"},{"issue":"3","key":"21_CR70","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10703-016-0259-2","volume":"49","author":"J Esparza","year":"2016","unstructured":"Esparza, J., Kret\u00ednsk\u00fd, J., Sickert, S.: From LTL to deterministic automata - a safraless compositional approach. Form. Methods Syst. Des. 49(3), 219\u2013271 (2016)","journal-title":"Form. Methods Syst. Des."},{"key":"21_CR71","unstructured":"Etessami, K.: Analysis of probabilistic processes and automata theory. In: Handbook of Automata Theory. European Mathematical Society (2016, to appear)"},{"key":"21_CR72","doi-asserted-by":"crossref","unstructured":"Etessami, K., Kwiatkowska, M.Z., Vardi, M.Y., Yannakakis, M.: Multi-objective model checking of Markov decision processes. Log. Methods Comput. Sci. 4(4) (2008)","DOI":"10.2168\/LMCS-4(4:8)2008"},{"issue":"2","key":"21_CR73","doi-asserted-by":"publisher","first-page":"11:1","DOI":"10.1145\/2699431","volume":"62","author":"K Etessami","year":"2015","unstructured":"Etessami, K., Yannakakis, M.: Recursive Markov decision processes and recursive stochastic games. J. ACM 62(2), 11:1\u201311:69 (2015)","journal-title":"J. ACM"},{"key":"21_CR74","doi-asserted-by":"crossref","unstructured":"Feinberg, E.A., Shwartz, A.: Methods and applications. In: Handbook of Markov Decision Processes. Kluwer (2002)","DOI":"10.1007\/978-1-4615-0805-2"},{"key":"21_CR75","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/978-3-642-24372-1_40","volume-title":"Automated Technology for Verification and Analysis","author":"L Feng","year":"2011","unstructured":"Feng, L., Han, T., Kwiatkowska, M., Parker, D.: Learning-based compositional verification for synchronous probabilistic systems. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 511\u2013521. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-24372-1_40"},{"issue":"1","key":"21_CR76","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s00165-016-0356-4","volume":"28","author":"LMF Fioriti","year":"2016","unstructured":"Fioriti, L.M.F., 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."},{"issue":"2","key":"21_CR77","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1145\/3149.214121","volume":"32","author":"MJ Fischer","year":"1985","unstructured":"Fischer, M.J., Lynch, N.A., Paterson, M.: Impossibility of distributed consensus with one faulty process. J. ACM 32(2), 374\u2013382 (1985)","journal-title":"J. ACM"},{"key":"21_CR78","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-642-19835-9_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V Forejt","year":"2011","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Quantitative multi-objective verification for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 112\u2013127. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-19835-9_11"},{"key":"21_CR79","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-642-54830-7_5","volume-title":"Foundations of Software Science and Computation Structures","author":"H Fu","year":"2014","unstructured":"Fu, H.: Maximal cost-bounded reachability probability on continuous-time Markov decision processes. In: Muscholl, A. (ed.) FoSSaCS 2014. LNCS, vol. 8412, pp. 73\u201387. Springer, Heidelberg (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-642-54830-7_5"},{"issue":"2\/3","key":"21_CR80","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1023\/A:1008647823331","volume":"10","author":"M Fujita","year":"1997","unstructured":"Fujita, M., McGeer, P.C., Yang, J.C.-Y.: Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. Form. Methods Syst. Des. 10(2\/3), 149\u2013169 (1997)","journal-title":"Form. Methods Syst. Des."},{"key":"21_CR81","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-319-04298-5_25","volume-title":"SOFSEM 2014: Theory and Practice of Computer Science","author":"H Gimbert","year":"2014","unstructured":"Gimbert, H., Oualhadj, Y.: Deciding the value 1 problem for \n                      \n                        \n                      \n                      $$\\sharp $$\n                    -acyclic partially observable Markov decision processes. In: Geffert, V., Preneel, B., Rovan, B., \u0160tuller, J., Tjoa, A.M. (eds.) SOFSEM 2014. LNCS, vol. 8327, pp. 281\u2013292. Springer, Cham (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-319-04298-5_25"},{"key":"21_CR82","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-642-04081-8_23","volume-title":"CONCUR 2009 - Concurrency Theory","author":"S Giro","year":"2009","unstructured":"Giro, S., D\u2019Argenio, P.R., Ferrer Fioriti, L.M.: Partial order reduction for probabilistic systems: a revision for distributed schedulers. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 338\u2013353. Springer, Heidelberg (2009). \n                      https:\/\/doi.org\/10.1007\/978-3-642-04081-8_23"},{"issue":"1\u20132","key":"21_CR83","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":"21_CR84","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1016\/j.peva.2013.11.004","volume":"73","author":"F Gretz","year":"2014","unstructured":"Gretz, F., Katoen, J.-P., McIver, A.: Operational versus weakest pre-expectation semantics for the probabilistic guarded command language. Perform. Eval. 73, 110\u2013132 (2014)","journal-title":"Perform. Eval."},{"key":"21_CR85","series-title":"Stochastic Modelling and Applied Probability","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02547-1","volume-title":"Continuous-Time Markov Decision Processes: Theory and Applications","author":"X Guo","year":"2009","unstructured":"Guo, X., Hernandez-Lerma, O.: Continuous-Time Markov Decision Processes: Theory and Applications. Stochastic Modelling and Applied Probability, vol. 62. Springer, Heidelberg (2009). \n                      https:\/\/doi.org\/10.1007\/978-3-642-02547-1"},{"key":"21_CR86","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/978-3-662-47666-6_19","volume-title":"Automata, Languages, and Programming","author":"C Haase","year":"2015","unstructured":"Haase, C., Kiefer, S.: The odds of staying on budget. In: Halld\u00f3rsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 234\u2013246. Springer, Heidelberg (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-662-47666-6_19"},{"issue":"12","key":"21_CR87","doi-asserted-by":"publisher","first-page":"1479","DOI":"10.1109\/43.552081","volume":"15","author":"GD Hachtel","year":"1996","unstructured":"Hachtel, G.D., Macii, E., Pardo, A., Somenzi, F.: Markovian analysis of large finite state machines. IEEE Trans. CAD Integr. Circ. Syst. 15(12), 1479\u20131493 (1996)","journal-title":"IEEE Trans. CAD Integr. Circ. Syst."},{"key":"21_CR88","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-319-11439-2_10","volume-title":"Reachability Problems","author":"S Haddad","year":"2014","unstructured":"Haddad, S., Monmege, B.: Reachability in MDPs: refining convergence of value iteration. In: Ouaknine, J., Potapov, I., Worrell, J. (eds.) RP 2014. LNCS, vol. 8762, pp. 125\u2013137. Springer, Cham (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-319-11439-2_10"},{"key":"21_CR89","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). \n                      https:\/\/doi.org\/10.1007\/978-3-642-20398-5_12"},{"issue":"4","key":"21_CR90","doi-asserted-by":"publisher","first-page":"1254","DOI":"10.1109\/TR.2015.2449292","volume":"64","author":"EM Hahn","year":"2015","unstructured":"Hahn, E.M., Hermanns, H., Wimmer, R., Becker, B.: Transient reward approximation for continuous-time Markov chains. IEEE Trans. Reliabil. 64(4), 1254\u20131275 (2015)","journal-title":"IEEE Trans. Reliabil."},{"key":"21_CR91","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-319-66335-7_13","volume-title":"Quantitative Evaluation of Systems","author":"EM Hahn","year":"2017","unstructured":"Hahn, E.M., Hashemi, V., Hermanns, H., Lahijanian, M., Turrini, A.: Multi-objective robust strategy synthesis for\u00a0interval Markov decision processes. In: Bertrand, N., Bortolussi, L. (eds.) QEST 2017. LNCS, vol. 10503, pp. 207\u2013223. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-66335-7_13"},{"key":"21_CR92","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-319-91908-9_18","volume-title":"Computing and Software Science","author":"R H\u00e4hnle","year":"2018","unstructured":"H\u00e4hnle, R., Huisman, M.: Deductive software verification: from pen-and-paper proofs to industrial tools. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 345\u2013373. Springer, Cham (2018)"},{"issue":"5","key":"21_CR93","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. Form. Asp. Comput. 6(5), 512\u2013535 (1994)","journal-title":"Form. Asp. Comput."},{"key":"21_CR94","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-319-24953-7_10","volume-title":"Automated Technology for Verification and Analysis","author":"A Hartmanns","year":"2015","unstructured":"Hartmanns, A., Hermanns, H.: Explicit model checking of very large MDP using partitioning and secondary storage. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 131\u2013147. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-24953-7_10"},{"issue":"4","key":"21_CR95","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/s10009-014-0349-7","volume":"17","author":"A Hartmanns","year":"2015","unstructured":"Hartmanns, A., Timmer, M.: Sound statistical model checking for MDP using partial order and confluence reduction. STTT 17(4), 429\u2013456 (2015)","journal-title":"STTT"},{"key":"21_CR96","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). \n                      https:\/\/doi.org\/10.1007\/978-3-319-30000-9_9"},{"key":"21_CR97","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-662-49122-5_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"V Hashemi","year":"2016","unstructured":"Hashemi, V., Hermanns, H., Song, L.: Reward-bounded reachability probability for uncertain weighted MDPs. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 351\u2013371. Springer, Heidelberg (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-662-49122-5_17"},{"key":"21_CR98","unstructured":"Hashemi, V.: Decision algorithms for modelling, optimal control and verification of probabilistic systems. Ph.D. thesis, Saarland University, Saarbr\u00fccken, Germany (2017)"},{"key":"21_CR99","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-662-44584-6_18","volume-title":"CONCUR 2014 \u2013 Concurrency Theory","author":"H Hermanns","year":"2014","unstructured":"Hermanns, H., Kr\u010d\u00e1l, J., K\u0159et\u00ednsk\u00fd, J.: Probabilistic bisimulation: naturally on distributions. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 249\u2013265. Springer, Heidelberg (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-662-44584-6_18"},{"issue":"2","key":"21_CR100","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1016\/j.ic.2010.11.024","volume":"209","author":"H Hermanns","year":"2011","unstructured":"Hermanns, H., Parma, A., Segala, R., Wachter, B., Zhang, L.: Probabilistic logical characterization. Inf. Comput. 209(2), 154\u2013172 (2011)","journal-title":"Inf. Comput."},{"key":"21_CR101","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-70545-1_16","volume-title":"Computer Aided Verification","author":"H Hermanns","year":"2008","unstructured":"Hermanns, H., Wachter, B., Zhang, L.: Probabilistic CEGAR. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 162\u2013175. Springer, Heidelberg (2008). \n                      https:\/\/doi.org\/10.1007\/978-3-540-70545-1_16"},{"key":"21_CR102","volume-title":"Dynamic Probabilistic Systems: Semi-Markov and Decision Processes","author":"RA Howard","year":"1972","unstructured":"Howard, R.A.: Dynamic Probabilistic Systems: Semi-Markov and Decision Processes, vol. 2. Wiley, New York (1972)"},{"issue":"6","key":"21_CR103","doi-asserted-by":"publisher","first-page":"816","DOI":"10.1177\/0278364914562980","volume":"34","author":"B Johnson","year":"2015","unstructured":"Johnson, B., Kress-Gazit, H.: Analyzing and revising synthesized controllers for robots with sensing and actuation errors. Int. J. Robot. Res. 34(6), 816\u2013832 (2015)","journal-title":"Int. J. Robot. Res."},{"key":"21_CR104","unstructured":"Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS, pp. 266\u2013277. IEEE Computer Society (1991)"},{"key":"21_CR105","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-662-49674-9_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Junges","year":"2016","unstructured":"Junges, S., Jansen, N., Dehnert, C., Topcu, U., Katoen, J.-P.: Safety-constrained reinforcement learning for MDPs. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 130\u2013146. Springer, Heidelberg (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-662-49674-9_8"},{"key":"21_CR106","unstructured":"Kallenberg, L.C.M.: Linear programming and finite Markovian control problems. Math. Center Tracts 148 (1983)"},{"key":"21_CR107","doi-asserted-by":"crossref","unstructured":"Katoen, J.-P.: The probabilistic model checking landscape. In: LICS, pp. 31\u201345. ACM (2016)","DOI":"10.1145\/2933575.2934574"},{"key":"21_CR108","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-319-23506-6_4","volume-title":"Correct System Design","author":"J-P Katoen","year":"2015","unstructured":"Katoen, J.-P., Gretz, F., Jansen, N., Kaminski, B.L., Olmedo, F.: Understanding probabilistic programs. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct System Design. LNCS, vol. 9360, pp. 15\u201332. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-23506-6_4"},{"issue":"4","key":"21_CR109","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1016\/j.jlap.2012.03.007","volume":"81","author":"J-P Katoen","year":"2012","unstructured":"Katoen, J.-P., Klink, D., Leucker, M., Wolf, V.: Three-valued abstraction for probabilistic systems. J. Log. Algebr. Program. 81(4), 356\u2013389 (2012)","journal-title":"J. Log. Algebr. Program."},{"issue":"3","key":"21_CR110","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/s10703-010-0097-6","volume":"36","author":"M Kattenbelt","year":"2010","unstructured":"Kattenbelt, M., Kwiatkowska, M.Z., Norman, G., Parker, D.: A game-based abstraction-refinement framework for Markov decision processes. Form. Methods Syst. Des. 36(3), 246\u2013280 (2010)","journal-title":"Form. Methods Syst. Des."},{"issue":"2","key":"21_CR111","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/j.peva.2010.04.002","volume":"68","author":"D Klink","year":"2011","unstructured":"Klink, D., Remke, A., Haverkort, B.R., Katoen, J.-P.: Time-bounded reachability in tree-structured QBDs by abstraction. Perform. Eval. 68(2), 105\u2013125 (2011)","journal-title":"Perform. Eval."},{"issue":"2","key":"21_CR112","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1016\/j.robot.2011.10.005","volume":"60","author":"S Konur","year":"2012","unstructured":"Konur, S., Dixon, C., Fisher, M.: Analysing robot swarm behaviour via probabilistic model checking. Robot. Auton. Syst. 60(2), 199\u2013213 (2012)","journal-title":"Robot. Auton. Syst."},{"key":"21_CR113","unstructured":"Kwiatkowska, M.Z.: Model checking for probability and time: from theory to practice. In: LICS, p. 351. IEEE Computer Society (2003)"},{"issue":"2","key":"21_CR114","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/s10009-004-0140-2","volume":"6","author":"MZ Kwiatkowska","year":"2004","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: a hybrid approach. STTT 6(2), 128\u2013142 (2004)","journal-title":"STTT"},{"key":"21_CR115","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/11817963_23","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Symmetry reduction for probabilistic model checking. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 234\u2013248. Springer, Heidelberg (2006). \n                      https:\/\/doi.org\/10.1007\/11817963_23"},{"key":"21_CR116","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). \n                      https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"21_CR117","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: The PRISM benchmark suite. In: QEST, pp. 203\u2013204. IEEE Computer Society (2012)","DOI":"10.1109\/QEST.2012.14"},{"issue":"1","key":"21_CR118","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0304-3975(01)00046-9","volume":"282","author":"MZ Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M.Z., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theoret. Comput. Sci. 282(1), 101\u2013150 (2002)","journal-title":"Theoret. Comput. Sci."},{"key":"21_CR119","unstructured":"Lacerda, B., Parker, D., Hawes, N.: Optimal policy generation for partially satisfiable co-safe LTL specifications. In: IJCAI, pp. 1587\u20131593. AAAI Press (2015)"},{"issue":"1","key":"21_CR120","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"KG Larsen","year":"1991","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1\u201328 (1991)","journal-title":"Inf. Comput."},{"key":"21_CR121","unstructured":"Larsen, K.G., Thomsen, B.: A modal process logic. In: LICS, pp. 203\u2013210. IEEE Computer Society (1988)"},{"issue":"1","key":"21_CR122","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/BF02055574","volume":"28","author":"WS Lovejoy","year":"1991","unstructured":"Lovejoy, W.S.: A survey of algorithmic methods for partially oberserved Markov decision processes. Ann. Oper. Res. 28(1), 47\u201365 (1991)","journal-title":"Ann. Oper. Res."},{"issue":"1\u20132","key":"21_CR123","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/S0004-3702(02)00378-8","volume":"147","author":"O Madani","year":"2003","unstructured":"Madani, O., Hanks, S., Condon, A.: On the undecidability of probabilistic planning and related stochastic optimization problems. Artif. Intell. 147(1\u20132), 5\u201334 (2003)","journal-title":"Artif. Intell."},{"issue":"2","key":"21_CR124","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/s10994-016-5565-9","volume":"105","author":"H Mao","year":"2016","unstructured":"Mao, H., Chen, Y., Jaeger, M., Nielsen, T.D., Larsen, K.G., Nielsen, B.: Learning deterministic probabilistic automata from a model checking perspective. Mach. Learn. 105(2), 255\u2013299 (2016)","journal-title":"Mach. Learn."},{"key":"21_CR125","doi-asserted-by":"crossref","unstructured":"Mayr, R., Schewe, S., Totzke, P., Wojitczak, D.: MDPs with energy-parity objectives. In: LICS, pp. 1\u201312. IEEE Computer Society (2017)","DOI":"10.1109\/LICS.2017.8005131"},{"key":"21_CR126","series-title":"Monographs in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/b138392","volume-title":"Abstraction, Refinement and Proof for Probabilistic Systems","author":"A McIver","year":"2005","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, New York (2005). \n                      https:\/\/doi.org\/10.1007\/b138392"},{"key":"21_CR127","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-642-00596-1_26","volume-title":"Foundations of Software Science and Computational Structures","author":"MR Neuh\u00e4u\u00dfer","year":"2009","unstructured":"Neuh\u00e4u\u00dfer, M.R., Stoelinga, M., Katoen, J.-P.: Delayed nondeterminism in continuous-time Markov decision processes. In: de Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 364\u2013379. Springer, Heidelberg (2009). \n                      https:\/\/doi.org\/10.1007\/978-3-642-00596-1_26"},{"key":"21_CR128","doi-asserted-by":"crossref","unstructured":"Neuh\u00e4u\u00dfer, M.R., Zhang, L.: Time-bounded reachability probabilities in continuous-time Markov decision processes. In: QEST, pp. 209\u2013218. IEEE Computer Society (2010)","DOI":"10.1109\/QEST.2010.47"},{"issue":"2","key":"21_CR129","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/s10703-012-0177-x","volume":"43","author":"G Norman","year":"2013","unstructured":"Norman, G., Parker, D., Sproston, J.: Model checking for probabilistic timed automata. Form. Methods Syst. Des. 43(2), 164\u2013190 (2013)","journal-title":"Form. Methods Syst. Des."},{"key":"21_CR130","unstructured":"Parker, D.: Implementation of symbolic model checking for probabilistic systems. Ph.D. thesis, University of Birmingham (2002)"},{"issue":"2","key":"21_CR131","doi-asserted-by":"publisher","first-page":"287","DOI":"10.3233\/AIC-150689","volume":"29","author":"S Pathak","year":"2016","unstructured":"Pathak, S., Pulina, L., Tacchella, A.: Evaluating probabilistic model checking tools for verification of robot control policies. AI Commun. 29(2), 287\u2013299 (2016)","journal-title":"AI Commun."},{"issue":"1","key":"21_CR132","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/BF01843570","volume":"1","author":"A Pnueli","year":"1986","unstructured":"Pnueli, A., Zuck, L.D.: Verification of multiprocess probabilistic protocols. Distrib. Comput. 1(1), 53\u201372 (1986)","journal-title":"Distrib. Comput."},{"key":"21_CR133","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"M Puterman","year":"1994","unstructured":"Puterman, M.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, New York (1994)"},{"key":"21_CR134","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-319-46520-3_4","volume-title":"Automated Technology for Verification and Analysis","author":"T Quatmann","year":"2016","unstructured":"Quatmann, T., Dehnert, C., Jansen, N., Junges, S., Katoen, J.-P.: Parameter synthesis for Markov models: faster than ever. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 50\u201367. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-46520-3_4"},{"key":"21_CR135","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-319-63387-9_7","volume-title":"Computer Aided Verification","author":"T Quatmann","year":"2017","unstructured":"Quatmann, T., Junges, S., Katoen, J.-P.: Markov automata with multiple objectives. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 140\u2013159. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-63387-9_7"},{"issue":"5\u20136","key":"21_CR136","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/s00236-011-0140-0","volume":"48","author":"MN Rabe","year":"2011","unstructured":"Rabe, M.N., Schewe, S.: Finite optimal control for time-bounded reachability in CTMDPs and continuous-time Markov games. Acta Inf. 48(5\u20136), 291\u2013315 (2011)","journal-title":"Acta Inf."},{"key":"21_CR137","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-319-21690-4_8","volume-title":"Computer Aided Verification","author":"M Randour","year":"2015","unstructured":"Randour, M., Raskin, J.-F., Sankur, O.: Percentile queries in multi-dimensional Markov decision processes. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 123\u2013139. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-21690-4_8"},{"key":"21_CR138","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1613\/jair.3987","volume":"48","author":"DM Roijers","year":"2013","unstructured":"Roijers, D.M., Vamplew, P., Whiteson, S., Dazeley, R.: A survey of multi-objective sequential decision-making. J. Artif. Intell. Res. 48, 67\u2013113 (2013)","journal-title":"J. Artif. Intell. Res."},{"key":"21_CR139","doi-asserted-by":"crossref","unstructured":"Scheftelowitsch, D., Buchholz, P., Hashemi, V., Hermanns, H.: Multi-objective approaches to Markov decision processes with uncertain transition parameters. In: Casale, G., Marin, A., Petriu, D., Rossi, S., Van Houdt, B. (eds.) 11th International Conference on Performance Evaluation Methodologies and Tools, VALUETOOLS 2017, Venice, Italy (2017)","DOI":"10.1145\/3150928.3150945"},{"key":"21_CR140","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1016\/j.ic.2014.02.001","volume":"237","author":"J Schuster","year":"2014","unstructured":"Schuster, J., Siegle, M.: Markov automata: deciding weak bisimulation by means of non-na\u00efvely vanishing states. Inf. Comput. 237, 151\u2013173 (2014)","journal-title":"Inf. Comput."},{"issue":"2","key":"21_CR141","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":"21_CR142","volume-title":"Reinforcement Learning: An Introduction","author":"RS Sutton","year":"1998","unstructured":"Sutton, R.S., Barto, A.G.: Reinforcement Learning: An Introduction. The MIT Press, Cambridge (1998)"},{"key":"21_CR143","unstructured":"Teichteil-K\u00f6nigsbuch, F.: Path-constrained Markov decision processes: bridging the gap between probabilistic model-checking and decision-theoretic planning. In: ECAI. Frontiers in AI and Applications, vol. 242, pp. 744\u2013749. IOS Press (2012)"},{"key":"21_CR144","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.ic.2016.11.006","volume":"253","author":"I Tkachev","year":"2017","unstructured":"Tkachev, I., Mereacre, A., Katoen, J.-P., Abate, A.: Quantitative model-checking of controlled discrete-time Markov processes. Inf. Comput. 253, 1\u201335 (2017)","journal-title":"Inf. Comput."},{"key":"21_CR145","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":"21_CR146","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-642-37075-5_23","volume-title":"Foundations of Software Science and Computation Structures","author":"M Ummels","year":"2013","unstructured":"Ummels, M., Baier, C.: Computing quantiles in Markov reward models. In: Pfenning, F. (ed.) FoSSaCS 2013. LNCS, vol. 7794, pp. 353\u2013368. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-37075-5_23"},{"key":"21_CR147","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: FOCS, pp. 327\u2013338. IEEE (1985)","DOI":"10.1109\/SFCS.1985.12"},{"key":"21_CR148","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: LICS, pp. 332\u2013344. IEEE Computer Society Press (1986)"},{"issue":"4","key":"21_CR149","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/s00236-015-0237-y","volume":"53","author":"C Essen von","year":"2016","unstructured":"von Essen, C., Jobstmann, B., Parker, D., Varshneya, R.: Synthesizing efficient systems in probabilistic environments. Acta Inf. 53(4), 425\u2013457 (2016)","journal-title":"Acta Inf."},{"key":"21_CR150","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/978-3-642-11319-2_26","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B Wachter","year":"2010","unstructured":"Wachter, B., Zhang, L.: Best probabilistic transformers. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 362\u2013379. Springer, Heidelberg (2010). \n                      https:\/\/doi.org\/10.1007\/978-3-642-11319-2_26"},{"issue":"11","key":"21_CR151","doi-asserted-by":"publisher","first-page":"1073","DOI":"10.1057\/jors.1993.181","volume":"44","author":"DJ White","year":"1993","unstructured":"White, D.J.: A survey of applications of Markov decision processes. J. Oper. Res. Soc. 44(11), 1073\u20131096 (1993)","journal-title":"J. Oper. Res. Soc."},{"issue":"3","key":"21_CR152","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/s10703-016-0246-7","volume":"48","author":"A Wijs","year":"2016","unstructured":"Wijs, A., Katoen, J.-P., Bosnacki, D.: Efficient GPU algorithms for parallel decomposition of graphs into strongly connected and maximal end components. Form. Methods Syst. Des. 48(3), 274\u2013300 (2016)","journal-title":"Form. Methods Syst. Des."},{"key":"21_CR153","doi-asserted-by":"crossref","unstructured":"Wimmer, R., Braitling, B., Becker, B., E., Hahn, M., Crouzen, P., Hermanns, H., Dhama, A., Theel, O.E.: Symblicit calculation of long-run averages for concurrent probabilistic systems. In: QEST, pp. 27\u201336. IEEE Computer Society (2010)","DOI":"10.1109\/QEST.2010.12"},{"key":"21_CR154","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.tcs.2014.06.020","volume":"549","author":"R Wimmer","year":"2014","unstructured":"Wimmer, R., Jansen, N., \u00c1brah\u00e1m, E., Katoen, J.-P., Becker, B.: Minimal counterexamples for linear-time probabilistic verification. Theor. Comput. Sci. 549, 61\u2013100 (2014)","journal-title":"Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Computing and Software Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-91908-9_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,30]],"date-time":"2019-10-30T11:02:33Z","timestamp":1572433353000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-91908-9_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783319919072","9783319919089"],"references-count":154,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-91908-9_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"5 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}