{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,2]],"date-time":"2026-08-02T15:35:48Z","timestamp":1785684948521,"version":"3.56.0"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030010898","type":"print"},{"value":"9783030010904","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[[2018]]},"DOI":"10.1007\/978-3-030-01090-4_10","type":"book-chapter","created":{"date-parts":[[2018,9,29]],"date-time":"2018-09-29T15:23:23Z","timestamp":1538234603000},"page":"160-176","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":24,"title":["Synthesis in pMDPs: A Tale of 1001 Parameters"],"prefix":"10.1007","author":[{"given":"Murat","family":"Cubuktepe","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nils","family":"Jansen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sebastian","family":"Junges","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ufuk","family":"Topcu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,9,30]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Aflaki, S., Volk, M., Bonakdarpour, B., Katoen, J.P., Storjohann, A.: Automated fine tuning of probabilistic self-stabilizing algorithms. In: SRDS, pp. 94\u2013103. IEEE CS (2017)","DOI":"10.1109\/SRDS.2017.22"},{"issue":"1","key":"10_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10107-002-0339-5","volume":"95","author":"F Alizadeh","year":"2003","unstructured":"Alizadeh, F., Goldfarb, D.: Second-order cone programming. Math. Program. 95(1), 3\u201351 (2003)","journal-title":"Math. Program."},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Amato, C., Bernstein, D.S., Zilberstein, S.: Solving POMDPs using quadratically constrained linear programs. In: AAMAS, pp. 341\u2013343. ACM (2006)","DOI":"10.1145\/1160633.1160694"},{"key":"10_CR4","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"10_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"},{"issue":"1","key":"10_CR6","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/s11081-007-9001-7","volume":"8","author":"Stephen Boyd","year":"2007","unstructured":"Boyd, S., Kim, S.J., Vandenberghe, L., Hassibi, A.: A tutorial on geometric programming. Optim. Eng. 8(1) (2007)","journal-title":"Optimization and Engineering"},{"key":"10_CR7","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511804441","volume-title":"Convex Optimization","author":"S Boyd","year":"2004","unstructured":"Boyd, S., Vandenberghe, L.: Convex Optimization. Cambridge University Press, New York (2004)"},{"key":"10_CR8","first-page":"373","volume-title":"Mixed Integer Nonlinear Programming","author":"Samuel Burer","year":"2011","unstructured":"Burer, S., Saxena, A.: The MILP road to MIQCP. Mixed Integer Nonlinear Programming, pp. 373\u2013405 (2012)"},{"issue":"9","key":"10_CR9","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/2330667.2330686","volume":"55","author":"R Calinescu","year":"2012","unstructured":"Calinescu, R., Ghezzi, C., Kwiatkowska, M., Mirandola, R.: Self-adaptive software needs quantitative verification at runtime. Commun. ACM 55(9), 69\u201377 (2012)","journal-title":"Commun. ACM"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Chen, T., Hahn, E.M., Han, T., Kwiatkowska, M., Qu, H., Zhang, L.: Model repair for Markov decision processes. In: TASE, pp. 85\u201392. IEEE CS (2013)","DOI":"10.1109\/TASE.2013.20"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.P., Topcu, U.: Synthesis in pMDPs: a tale of 1001 parameters. CoRR abs\/1803.02884 (2018)","DOI":"10.1007\/978-3-030-01090-4_10"},{"key":"10_CR12","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., et al.: 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":"10_CR13","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":"10_CR14","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":"10_CR15","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":"83","key":"10_CR16","first-page":"1","volume":"17","author":"S Diamond","year":"2016","unstructured":"Diamond, S., Boyd, S.: CVXPY: a python-embedded modeling language for convex optimization. J. Mach. Learn. Res. 17(83), 1\u20135 (2016)","journal-title":"J. Mach. Learn. Res."},{"issue":"6","key":"10_CR17","first-page":"195","volume":"128","author":"M Duflot","year":"2005","unstructured":"Duflot, M., et al.: Probabilistic model checking of the CSMA\/CD protocol using PRISM and APMC. Electr. Notes TCS 128(6), 195\u2013214 (2005)","journal-title":"Electr. Notes TCS"},{"issue":"1","key":"10_CR18","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1109\/TSE.2015.2421318","volume":"42","author":"A Filieri","year":"2016","unstructured":"Filieri, A., Tamburrelli, G., Ghezzi, C.: Supporting self-adaptation via quantitative verification and sensitivity analysis at run time. IEEE Trans. Softw. Eng. 42(1), 75\u201399 (2016)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Gainer, P., Hahn, E.M., Schewe, S.: Incremental verification of parametric and reconfigurable Markov chains. CoRR abs\/1804.01872 (2018)","DOI":"10.1007\/978-3-319-99154-2_9"},{"key":"10_CR20","unstructured":"Gurobi Optimization Inc.: Gurobi optimizer reference manual. http:\/\/www.gurobi.com (2013)"},{"key":"10_CR21","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"},{"issue":"1","key":"10_CR22","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10009-010-0146-x","volume":"13","author":"EM Hahn","year":"2010","unstructured":"Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. STTT 13(1), 3\u201319 (2010)","journal-title":"STTT"},{"key":"10_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-319-06410-9_22","volume-title":"FM 2014: Formal Methods","author":"EM Hahn","year":"2014","unstructured":"Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: iscasMc: a web-based probabilistic model checker. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 312\u2013317. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_22"},{"key":"10_CR24","doi-asserted-by":"publisher","first-page":"16","DOI":"10.4204\/EPTCS.256.2","volume":"256","author":"L Hutschenreiter","year":"2017","unstructured":"Hutschenreiter, L., Baier, C., Klein, J.: Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination. GandALF. EPTCS 256, 16\u201330 (2017)","journal-title":"GandALF. EPTCS"},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-642-31365-3_27","volume-title":"Automated Reasoning","author":"D Jovanovi\u0107","year":"2012","unstructured":"Jovanovi\u0107, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 339\u2013354. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_27"},{"key":"10_CR26","unstructured":"Junges, S., et al.: Finite-state controllers of POMDPs using parameter synthesis. In: UAI. AUAI Press, Canada (2018), to appear"},{"key":"10_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"issue":"1","key":"10_CR28","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."},{"issue":"2","key":"10_CR29","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/s10107-005-0582-7","volume":"103","author":"J Linderoth","year":"2005","unstructured":"Linderoth, J.: A simplicial branch-and-bound algorithm for solving quadratically constrained quadratic programs. Math. Program. 103(2), 251\u2013282 (2005)","journal-title":"Math. Program."},{"issue":"2","key":"10_CR30","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s11081-015-9294-x","volume":"17","author":"T Lipp","year":"2016","unstructured":"Lipp, T., Boyd, S.: Variations and extension of the convex-concave procedure. Optim. Eng. 17(2), 263\u2013287 (2016)","journal-title":"Optim. Eng."},{"issue":"3","key":"10_CR31","doi-asserted-by":"publisher","first-page":"1042","DOI":"10.1007\/s10957-016-0892-3","volume":"169","author":"B O\u2019Donoghue","year":"2016","unstructured":"O\u2019Donoghue, B., Chu, E., Parikh, N., Boyd, S.: Conic optimization via operator splitting and homogeneous self-dual embedding. J. Optim. Theory Appl. 169(3), 1042\u20131068 (2016)","journal-title":"J. Optim. Theory Appl."},{"key":"10_CR32","unstructured":"Park, J., Boyd, S.: General heuristics for nonconvex quadratically constrained quadratic programming. arXiv preprint arXiv:1703.07870 (2017)"},{"key":"10_CR33","doi-asserted-by":"crossref","unstructured":"Shen, X., Diamond, S., Gu, Y., Boyd, S.: Disciplined convex-concave programming. In: CDC, pp. 1009\u20131014. IEEE (2016)","DOI":"10.1109\/CDC.2016.7798400"},{"key":"10_CR34","doi-asserted-by":"crossref","unstructured":"Su, G., Rosenblum, D.S., Tamburrelli, G.: Reliability of run-time quality-of-service evaluation using parametric model checking. In: ICSE, pp. 073\u201384. ACM (2016)","DOI":"10.1145\/2884781.2884814"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-01090-4_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,25]],"date-time":"2019-10-25T03:32:35Z","timestamp":1571974355000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-01090-4_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030010898","9783030010904"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-01090-4_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 October 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 October 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/atva-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}