{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,30]],"date-time":"2026-08-30T01:05:39Z","timestamp":1788051939183,"version":"build-2784847793"},"reference-count":65,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"12","license":[{"start":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T00:00:00Z","timestamp":1669852800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T00:00:00Z","timestamp":1669852800000},"content-version":"am","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T00:00:00Z","timestamp":1669852800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T00:00:00Z","timestamp":1669852800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/501100008982","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1652113"],"award-info":[{"award-number":["1652113"]}],"id":[{"id":"10.13039\/501100008982","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"ONR","doi-asserted-by":"publisher","award":["N000141613165"],"award-info":[{"award-number":["N000141613165"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000104","name":"NASA","doi-asserted-by":"publisher","award":["NNX17AD04G"],"award-info":[{"award-number":["NNX17AD04G"]}],"id":[{"id":"10.13039\/100000104","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006602","name":"Air Force Research Laboratory","doi-asserted-by":"publisher","award":["FA8650-15-C-2546"],"award-info":[{"award-number":["FA8650-15-C-2546"]}],"id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Automat. Contr."],"published-print":{"date-parts":[[2022,12]]},"DOI":"10.1109\/tac.2021.3133265","type":"journal-article","created":{"date-parts":[[2021,12,7]],"date-time":"2021-12-07T20:30:09Z","timestamp":1638909009000},"page":"6333-6348","source":"Crossref","is-referenced-by-count":17,"title":["Convex Optimization for Parameter Synthesis in MDPs"],"prefix":"10.1109","volume":"67","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0409-2403","authenticated-orcid":false,"given":"Murat","family":"Cubuktepe","sequence":"first","affiliation":[{"name":"Department of Aerospace Engineering and Engineering Mechanics, University of Texas at Austin, Austin, TX, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1318-8973","authenticated-orcid":false,"given":"Nils","family":"Jansen","sequence":"additional","affiliation":[{"name":"Institute for Computing and Information Science, Radboud University Nijmegen, Nijmegen, The Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0978-8466","authenticated-orcid":false,"given":"Sebastian","family":"Junges","sequence":"additional","affiliation":[{"name":"Institute for Computing and Information Science, Radboud University Nijmegen, Nijmegen, The Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[{"name":"Departement of Computer Science, RWTH Aachen University, Aachen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0819-9985","authenticated-orcid":false,"given":"Ufuk","family":"Topcu","sequence":"additional","affiliation":[{"name":"Department of Aerospace Engineering and Engineering Mechanics, University of Texas at Austin, Austin, TX, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_35"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2013.01.004"},{"key":"ref33","article-title":"Parameter synthesis for Markov models","author":"junges","year":"2019"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31784-3_28"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46520-3_4"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2019.104504"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_26"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45190-5_16"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_32"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89963-3_23"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.2514\/6.2020-0877"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.2514\/4.860119"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.2514\/1.G000115"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1109\/AERO.2007.352811"},{"key":"ref28","doi-asserted-by":"crossref","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","article-title":"4.0: Verification of probabilistic real-time systems","volume":"6806","author":"kwiatkowska","year":"2011","journal-title":"Computer Aided Verification"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1016\/B978-1-55860-307-3.50031-9"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2015.2421318"},{"key":"ref65","first-page":"1","article-title":"Real-time scheduling over Markovian channels: When partial observability meets hard deadlines","author":"yang","year":"0","journal-title":"Proc IEEE Glob Telecommun Conf"},{"key":"ref29","first-page":"592","article-title":"A storm is coming: A modern probabilistic model checker","volume":"10427","author":"dehnert","year":"2017","journal-title":"Computer Aided Verification (2)"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2014.2298143"},{"key":"ref1","doi-asserted-by":"crossref","DOI":"10.1002\/9780470316887","author":"puterman","year":"1994","journal-title":"Markov Decision Processes Discrete Stochastic Dynamic Programming"},{"key":"ref20","article-title":"Gurobi optimizer reference manual","year":"2021"},{"key":"ref22","article-title":"Parameter synthesis in Markov models","author":"junges","year":"2020"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4_10"},{"key":"ref24","article-title":"Successive convexification: A superlinearly convergent algorithm for non-convex optimal control problems","author":"mao","year":"2018"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/s10107-015-0893-2"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_13"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1137\/120871390"},{"key":"ref50","first-page":"1759","article-title":"On the convergence of the concave-convex procedure","author":"lanckriet","year":"0","journal-title":"Proc Adv Neural Inf Process Syst"},{"key":"ref51","first-page":"2601","article-title":"Convergence guarantees for a class of non-convex and non-smooth optimization problems","author":"khamaru","year":"0","journal-title":"Proc Int Conf Mach Learn"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.2514\/1.G002914"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1007\/s11241-017-9269-4"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1007\/BF01588250"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.1987.1104615"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1287\/mnsc.31.10.1312"},{"key":"ref54","author":"rudin","year":"1976","journal-title":"Principles of Mathematical Analysis"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.5802\/aif.1638"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1007\/s10957-012-0145-z"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884814"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/SRDS.2017.22"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66335-7_13"},{"key":"ref12","first-page":"519","article-title":"Finite-state controllers of POMDPs using parameter synthesis","author":"junges","year":"0","journal-title":"Proc Conf Uncertainty Artif Intell"},{"key":"ref13","first-page":"14:1","article-title":"On the complexity of reachability in parametric Markov decision processes","volume":"140","author":"winkler","year":"0","journal-title":"Proc 30th Int Conf Concurrency Theory"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19835-9_30"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_12"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2013.20"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/s10107-002-0339-5"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1016\/S0024-3795(98)10032-0"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/s11081-015-9294-x"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.15607\/RSS.2018.XIV.047"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_54"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31862-0_21"},{"key":"ref5","author":"baier","year":"2008","journal-title":"Principles of Model Checking"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0146-x"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-006-0015-2"},{"key":"ref49","first-page":"1033","article-title":"The concave–convex procedure (CCCP)","author":"yuille","year":"0","journal-title":"Proc Adv Neural Inf Process Syst"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/2330667.2330686"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54580-5_8"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v35i13.17401"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1287\/moor.2015.0735"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511804441"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1145\/1160633.1160694"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2007.12.002"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2020\/569"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1007\/s10458-009-9103-z"}],"container-title":["IEEE Transactions on Automatic Control"],"original-title":[],"link":[{"URL":"https:\/\/ieeexplore.ieee.org\/ielam\/9\/9969927\/9640499-aam.pdf","content-type":"application\/pdf","content-version":"am","intended-application":"syndication"},{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9\/9969927\/09640499.pdf?arnumber=9640499","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,26]],"date-time":"2022-12-26T19:31:48Z","timestamp":1672083108000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9640499\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,12]]},"references-count":65,"journal-issue":{"issue":"12"},"URL":"https:\/\/doi.org\/10.1109\/tac.2021.3133265","relation":{},"ISSN":["0018-9286","1558-2523","2334-3303"],"issn-type":[{"value":"0018-9286","type":"print"},{"value":"1558-2523","type":"electronic"},{"value":"2334-3303","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,12]]}}}