{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T20:00:34Z","timestamp":1743105634203,"version":"3.40.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031757747"},{"type":"electronic","value":"9783031757754"}],"license":[{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-75775-4_7","type":"book-chapter","created":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T07:26:57Z","timestamp":1731396417000},"page":"145-165","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Analyzing Value Functions of\u00a0States in\u00a0Parametric Markov Chains"],"prefix":"10.1007","author":[{"given":"Kasper","family":"Engelen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guillermo A.","family":"P\u00e9rez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shrisha","family":"Rao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,11,13]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","unstructured":"Aflaki, S., Volk, M., Bonakdarpour, B., Katoen, J., Storjohann, A.: Automated fine tuning of probabilistic self-stabilizing algorithms. In: 36th IEEE Symposium on Reliable Distributed Systems, SRDS 2017, Hong Kong, September 26-29, 2017, pp. 94\u2013103. IEEE Computer Society (2017)). https:\/\/doi.org\/10.1109\/SRDS.2017.22","DOI":"10.1109\/SRDS.2017.22"},{"key":"7_CR2","doi-asserted-by":"publisher","first-page":"104504","DOI":"10.1016\/J.IC.2019.104504","volume":"272","author":"C Baier","year":"2020","unstructured":"Baier, C., Hensel, C., Hutschenreiter, L., Junges, S., Katoen, J., Klein, J.: Parametric Markov chains: PCTL complexity and fraction-free gaussian elimination. Inf. Comput. 272, 104504 (2020). https:\/\/doi.org\/10.1016\/J.IC.2019.104504","journal-title":"Inf. Comput."},{"key":"7_CR3","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press (2008)"},{"issue":"1","key":"7_CR4","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1093\/imamat\/10.1.68","volume":"10","author":"EH Bareiss","year":"1972","unstructured":"Bareiss, E.H.: Computational solutions of matrix problems over an integral domain. IMA J. Appl. Math. 10(1), 68\u2013104 (1972). https:\/\/doi.org\/10.1093\/imamat\/10.1.68","journal-title":"IMA J. Appl. Math."},{"key":"7_CR5","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":"7_CR6","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/0304-3975(83)90110-X","volume":"22","author":"W Baur","year":"1983","unstructured":"Baur, W., Strassen, V.: The complexity of partial derivatives. Theor. Comput. Sci. 22, 317\u2013330 (1983)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"7_CR7","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1137\/0221006","volume":"21","author":"M Ben-Or","year":"1992","unstructured":"Ben-Or, M., Cleve, R.: Computing algebraic formulas using a constant number of registers. SIAM J. Comput. 21(1), 54\u201358 (1992)","journal-title":"SIAM J. Comput."},{"issue":"1","key":"7_CR8","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/J.IC.2018.02.019","volume":"259","author":"G Chatzieleftheriou","year":"2018","unstructured":"Chatzieleftheriou, G., Katsaros, P.: Abstract model repair for probabilistic systems. Inf. Comput. 259(1), 142\u2013160 (2018). https:\/\/doi.org\/10.1016\/J.IC.2018.02.019","journal-title":"Inf. Comput."},{"key":"7_CR9","doi-asserted-by":"publisher","unstructured":"Chen, T., Hahn, E.M., Han, T., Kwiatkowska, M.Z., Qu, H., Zhang, L.: Model repair for Markov decision processes. In: Seventh International Symposium on Theoretical Aspects of Software Engineering, TASE 2013, 1-3 July 2013, Birmingham, UK, pp. 85\u201392. IEEE Computer Society (2013). https:\/\/doi.org\/10.1109\/TASE.2013.20","DOI":"10.1109\/TASE.2013.20"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-030-30806-3_7","volume-title":"Reachability Problems","author":"V Chonev","year":"2019","unstructured":"Chonev, V.: Reachability in augmented interval Markov chains. In: Filiot, E., Jungers, R., Potapov, I. (eds.) RP 2019. LNCS, vol. 11674, pp. 79\u201392. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30806-3_7"},{"key":"7_CR11","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":"7_CR12","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":"7_CR13","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"},{"key":"7_CR14","doi-asserted-by":"publisher","unstructured":"Engelen, K., Perez, G., Rao, S.: Code for: Analyzing value functions of states in parametric Markov chains (2024). https:\/\/doi.org\/10.5281\/zenodo.11474465","DOI":"10.5281\/zenodo.11474465"},{"key":"7_CR15","doi-asserted-by":"publisher","unstructured":"Engelen, K., P\u00e9rez, G.A., Rao, S.: Graph-based reductions for parametric and weighted MDPS. In: Andr\u00e9, \u00c9., Sun, J. (eds.) Automated Technology for Verification and Analysis. ATVA 2023. LNCS, vol. 14215. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-45329-8_7","DOI":"10.1007\/978-3-031-45329-8_7"},{"key":"7_CR16","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1016\/J.PEVA.2018.11.006","volume":"130","author":"A Gouberman","year":"2019","unstructured":"Gouberman, A., Siegle, M., Tati, B.: Markov chains with perturbed rates to absorption: theory and application to model repair. Perform. Eval. 130, 32\u201350 (2019). https:\/\/doi.org\/10.1016\/J.PEVA.2018.11.006","journal-title":"Perform. Eval."},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"660","DOI":"10.1007\/978-3-642-14295-6_56","volume-title":"Computer Aided Verification","author":"EM Hahn","year":"2010","unstructured":"Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: PARAM: a model checker for parametric Markov models. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 660\u2013664. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_56"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-030-94583-1_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L Heck","year":"2022","unstructured":"Heck, L., Spel, J., Junges, S., Moerman, J., Katoen, J.P.: Gradient-descent for randomized controllers under partial observability. In: Finkbeiner, B., Wies, T. (eds.) VMCAI 2022. LNCS, vol. 13182, pp. 127\u2013150. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_7"},{"key":"7_CR19","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/J.JCSS.2021.02.006","volume":"119","author":"S Junges","year":"2021","unstructured":"Junges, S., Katoen, J., P\u00e9rez, G.A., Winkler, T.: The complexity of reachability in parametric Markov decision processes. J. Comput. Syst. Sci. 119, 183\u2013210 (2021). https:\/\/doi.org\/10.1016\/J.JCSS.2021.02.006","journal-title":"J. Comput. Syst. Sci."},{"key":"7_CR20","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":"7_CR21","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. Formal Aspects Comput. 19(1), 93\u2013109 (2007). https:\/\/doi.org\/10.1007\/S00165-006-0015-2","journal-title":"Formal Aspects Comput."},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Mahajan, M.: Algebraic complexity classes. arXiv preprint arXiv:1307.3863 (2013)","DOI":"10.1007\/978-3-319-05446-9_4"},{"issue":"4","key":"7_CR23","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1145\/382242.382836","volume":"16","author":"J Morgenstern","year":"1985","unstructured":"Morgenstern, J.: How to compute fast a function and all its derivatives: a variation on the theorem of Baur-Strassen. SIGACT News 16(4), 60\u201362 (1985)","journal-title":"SIGACT News"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Nisan, N.: Lower bounds for non-commutative computation (extended abstract). In: STOC, pp. 410\u2013418. ACM (1991)","DOI":"10.1145\/103418.103462"},{"key":"7_CR25","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":"7_CR26","doi-asserted-by":"publisher","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley Series in Probability and Statistics. Wiley (1994). https:\/\/doi.org\/10.1002\/9780470316887","DOI":"10.1002\/9780470316887"},{"key":"7_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-319-89366-2_20","volume-title":"Foundations of Software Science and Computation Structures","author":"S Le Roux","year":"2018","unstructured":"Le Roux, S., P\u00e9rez, G.A.: The complexity of graph-based reductions for reachability in Markov decision processes. In: Baier, C., Dal Lago, U. (eds.) FoSSaCS 2018. LNCS, vol. 10803, pp. 367\u2013383. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89366-2_20"},{"key":"7_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-642-11805-0_32","volume-title":"Graph Drawing","author":"M Schaefer","year":"2010","unstructured":"Schaefer, M.: Complexity of some geometric and topological problems. In: Eppstein, D., Gansner, E.R. (eds.) GD 2009. LNCS, vol. 5849, pp. 334\u2013344. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11805-0_32"},{"key":"7_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-030-31784-3_28","volume-title":"Automated Technology for Verification and Analysis","author":"J Spel","year":"2019","unstructured":"Spel, J., Junges, S., Katoen, J.P.: Are parametric Markov chains monotonic? In: Chen, Y.F., Cheng, C.H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 479\u2013496. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_28"},{"key":"7_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-030-72016-2_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Spel","year":"2021","unstructured":"Spel, J., Junges, S., Katoen, J.-P.: Finding provably optimal Markov chains. In: TACAS 2021. LNCS, vol. 12651, pp. 173\u2013190. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_10"},{"key":"7_CR31","doi-asserted-by":"crossref","unstructured":"Strassen, V.: Vermeidung von divisionen. J. f\u00fcr die reine und angewandte Math. 264, 184\u2013202 (1973). http:\/\/eudml.org\/doc\/151394","DOI":"10.1515\/crll.1973.264.184"},{"issue":"4","key":"7_CR32","doi-asserted-by":"publisher","first-page":"641","DOI":"10.1137\/0212043","volume":"12","author":"LG Valiant","year":"1983","unstructured":"Valiant, L.G., Skyum, S., Berkowitz, S., Rackoff, C.: Fast parallel computation of polynomials using few processors. SIAM J. Comput. 12(4), 641\u2013644 (1983). https:\/\/doi.org\/10.1137\/0212043","journal-title":"SIAM J. Comput."}],"container-title":["Lecture Notes in Computer Science","Principles of Verification: Cycling the Probabilistic Landscape"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-75775-4_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T08:03:28Z","timestamp":1731398608000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-75775-4_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,13]]},"ISBN":["9783031757747","9783031757754"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-75775-4_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,11,13]]},"assertion":[{"value":"13 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}