{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T11:30:45Z","timestamp":1768908645626,"version":"3.49.0"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319991535","type":"print"},{"value":"9783319991542","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-99154-2_4","type":"book-chapter","created":{"date-parts":[[2018,8,14]],"date-time":"2018-08-14T18:14:35Z","timestamp":1534270475000},"page":"53-70","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Parameter-Independent Strategies for pMDPs via POMDPs"],"prefix":"10.1007","author":[{"given":"Sebastian","family":"Arming","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ezio","family":"Bartocci","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Krishnendu","family":"Chatterjee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ana","family":"Sokolova","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,8,15]]},"reference":[{"key":"4_CR1","unstructured":"Arming, S., Bartocci, E., Chatterjee, K., Katoen, J., Sokolova, A.: Parameter-independent strategies for pMDPs via POMDPs. arXiv 1806.05126 (2018). http:\/\/arxiv.org\/abs\/1806.05126"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Arming, S., Bartocci, E., Sokolova, A.: SEA-PARAM: exploring schedulers in parametric MDPs. In: Proceedings of the QAPL 2017. EPTCS, vol. 250, pp. 25\u201338 (2017)","DOI":"10.4204\/EPTCS.250.3"},{"issue":"3","key":"4_CR3","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1016\/0196-6774(90)90021-6","volume":"11","author":"J Aspnes","year":"1990","unstructured":"Aspnes, J., Herlihy, M.: Fast randomized consensus using shared memory. J. Algorithms 11(3), 441\u2013461 (1990)","journal-title":"J. Algorithms"},{"issue":"1","key":"4_CR4","doi-asserted-by":"publisher","first-page":"1:1","DOI":"10.1145\/2108242.2108243","volume":"59","author":"C Baier","year":"2012","unstructured":"Baier, C., Gr\u00f6\u00dfer, M., Bertrand, N.: Probabilistic $$\\omega $$-automata. J. ACM 59(1), 1:1\u20131:52 (2012)","journal-title":"J. ACM"},{"key":"4_CR5","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-319-66335-7_8","volume-title":"Quantitative Evaluation of Systems","author":"M Baldi","year":"2017","unstructured":"Baldi, M., et al.: A probabilistic small model theorem to assess confidentiality of dispersed cloud storage. In: Bertrand, N., Bortolussi, L. (eds.) QEST 2017. LNCS, vol. 10503, pp. 123\u2013139. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66335-7_8"},{"key":"4_CR7","unstructured":"Bargiacchi, E.: AI-Toolbox. https:\/\/github.com\/Svalorzen\/AI-Toolbox\/"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-642-19835-9_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Bartocci","year":"2011","unstructured":"Bartocci, E., Grosu, R., Katsaros, P., Ramakrishnan, C.R., Smolka, S.A.: Model repair for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 326\u2013340. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_30"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-319-23404-5_12","volume-title":"Model Checking Software","author":"D Beyer","year":"2015","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Benchmarking and resource measurement. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, vol. 9232, pp. 160\u2013178. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23404-5_12"},{"key":"4_CR10","unstructured":"Cassandra, A.R., Littman, M.L., Zhang, N.L.: Incremental pruning - a simple, fast, exact method for partially observable Markov decision processes. In: Proceedings of the UAI 1997, pp. 54\u201361 (1997)"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-15155-2_24","volume-title":"Mathematical Foundations of Computer Science 2010","author":"K Chatterjee","year":"2010","unstructured":"Chatterjee, K., Doyen, L., Henzinger, T.A.: Qualitative analysis of partially-observable Markov decision processes. In: Hlin\u011bn\u00fd, P., Ku\u010dera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 258\u2013269. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15155-2_24"},{"key":"4_CR12","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1016\/j.artint.2014.12.009","volume":"221","author":"K Chatterjee","year":"2015","unstructured":"Chatterjee, K., Chmelik, M.: POMDPs under probabilistic semantics. Artif. Intell. 221, 46\u201372 (2015)","journal-title":"Artif. Intell."},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Chmelik, M., Davies, J.: A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs. In: Proceedings of the AAAI 2016, pp. 3225\u20133232 (2016)","DOI":"10.1609\/aaai.v30i1.10422"},{"key":"4_CR14","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."},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-15155-2_23","volume-title":"Mathematical Foundations of Computer Science 2010","author":"K Chatterjee","year":"2010","unstructured":"Chatterjee, K., Doyen, L., Gimbert, H., Henzinger, T.A.: Randomness for free. In: Hlin\u011bn\u00fd, P., Ku\u010dera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 246\u2013257. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15155-2_23"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Chen, T., Hahn, E.M., Han, T., Kwiatkowska, M.Z., Qu, H., Zhang, L.: Model repair for Markov decision processes. In: Proceedings of the TASE 2013, pp. 85\u201392 (2013)","DOI":"10.1109\/TASE.2013.20"},{"key":"4_CR17","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.: 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). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_8"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-31862-0_21","volume-title":"Theoretical Aspects of Computing - ICTAC 2004","author":"C Daws","year":"2005","unstructured":"Daws, C.: Symbolic and parametric model checking of discrete-time Markov chains. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 280\u2013294. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31862-0_21"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-319-21690-4_13","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2015","unstructured":"Dehnert, C., et al.: PROPhESY: a probabilistic parameter synthesis tool. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 214\u2013231. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_13"},{"key":"4_CR20","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). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31"},{"issue":"1","key":"4_CR21","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10009-010-0146-x","volume":"13","author":"EM Hahn","year":"2011","unstructured":"Hahn, E.M., Han, T., Zhang, L.: Probabilistic reachability for parametric Markov models. STTT 13(1), 3\u201319 (2011)","journal-title":"STTT"},{"key":"4_CR22","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). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_12"},{"key":"4_CR23","unstructured":"Hahn, E.M., Hermanns, H., Zhang, L., Wachter, B.: PARAM case studies (2015). https:\/\/depend.cs.uni-saarland.de\/tools\/param\/casestudies"},{"key":"4_CR24","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-9440-2","volume-title":"Measure Theory","author":"PR Halmos","year":"1974","unstructured":"Halmos, P.R.: Measure Theory. Springer, New York (1974). https:\/\/doi.org\/10.1007\/978-1-4684-9440-2"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-319-10696-0_31","volume-title":"Quantitative Evaluation of Systems","author":"N Jansen","year":"2014","unstructured":"Jansen, N., et al.: Accelerating parametric probabilistic verification. In: Norman, G., Sanders, W. (eds.) QEST 2014. LNCS, vol. 8657, pp. 404\u2013420. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10696-0_31"},{"key":"4_CR26","unstructured":"Junges, S., Jansen, N., Wimmer, R., Quatmann, T., Winterer, L., Katoen, J., Becker, B.: Finite-state controllers of POMDPs via parameter synthesis. In: Proceedings of the UAI 2018 (2018)"},{"key":"4_CR27","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-2793-7","volume-title":"Computational Complexity and Feasibility of Data Processing and Interval Computations, Applied Optimization","author":"V Kreinovich","year":"1998","unstructured":"Kreinovich, V., Lakeyev, A., Rohn, J., Kahl, P.: Computational Complexity and Feasibility of Data Processing and Interval Computations, Applied Optimization, vol. 10. Springer, Boston (1998). https:\/\/doi.org\/10.1007\/978-1-4757-2793-7"},{"key":"4_CR28","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). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"issue":"1","key":"4_CR29","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/s00165-006-0015-2","volume":"19","author":"R Lanotte","year":"2007","unstructured":"Lanotte, R., Maggiolo-Schettini, A., Troina, A.: Parametric probabilistic transition systems for system design and analysis. Form. Asp. Comput. 19(1), 93\u2013109 (2007)","journal-title":"Form. Asp. Comput."},{"key":"4_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/978-3-662-54580-5_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Lukina","year":"2017","unstructured":"Lukina, A., et al.: ARES: adaptive receding-horizon synthesis of optimal plans. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 286\u2013302. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_17"},{"issue":"1\u20132","key":"4_CR31","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."},{"key":"4_CR32","doi-asserted-by":"crossref","unstructured":"Medina Ayala, A.I., Andersson, S.B., Belta, C.: Probabilistic control from time-bounded temporal logic specifications in dynamic environments. In: Proceedings of the ICRA 2012, pp. 4705\u20134710. IEEE (2012)","DOI":"10.1109\/ICRA.2012.6224963"},{"key":"4_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-319-17524-9_21","volume-title":"NASA Formal Methods","author":"S Pathak","year":"2015","unstructured":"Pathak, S., \u00c1brah\u00e1m, E., Jansen, N., Tacchella, A., Katoen, J.-P.: A greedy approach for the efficient repair of stochastic models. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 295\u2013309. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_21"},{"key":"4_CR34","unstructured":"Pineau, J., Gordon, G.J., Thrun, S.: Point-based value iteration - an anytime algorithm for POMDPs. In: Proceedings of the IJCAI 2003, pp. 1025\u20131032 (2003)"},{"key":"4_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/978-3-319-66335-7_16","volume-title":"Quantitative Evaluation of Systems","author":"E Polgreen","year":"2017","unstructured":"Polgreen, E., Wijesuriya, V.B., Haesaert, S., Abate, A.: Automated experiment design for data-efficient verification of parametric Markov decision processes. In: Bertrand, N., Bortolussi, L. (eds.) QEST 2017. LNCS, vol. 10503, pp. 259\u2013274. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66335-7_16"},{"key":"4_CR36","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). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_4"},{"key":"4_CR37","volume-title":"Artificial Intelligence: A Modern Approach","author":"S Russell","year":"2009","unstructured":"Russell, S., Norvig, P.: Artificial Intelligence: A Modern Approach. Prentice Hall, Upper Saddle River (2009)"},{"key":"4_CR38","doi-asserted-by":"publisher","DOI":"10.1002\/9780470317037","volume-title":"Stochastic Dynamic Programming and the Control of Queueing Systems","author":"LI Sennott","year":"1998","unstructured":"Sennott, L.I.: Stochastic Dynamic Programming and the Control of Queueing Systems. Wiley, New York (1998)"},{"key":"4_CR39","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1613\/jair.1659","volume":"24","author":"MTJ Spaan","year":"2011","unstructured":"Spaan, M.T.J., Vlassis, N.: Perseus: randomized point-based value iteration for POMDPs. J. Artif. Intell. Res. 24, 195\u2013220 (2011)","journal-title":"J. Artif. Intell. Res."}],"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-99154-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,29]],"date-time":"2022-08-29T07:27:13Z","timestamp":1661758033000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99154-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319991535","9783319991542"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99154-2_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}