{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,31]],"date-time":"2026-01-31T05:06:45Z","timestamp":1769836005828,"version":"3.49.0"},"reference-count":40,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"8","license":[{"start":{"date-parts":[[2015,8,1]],"date-time":"2015-08-01T00:00:00Z","timestamp":1438387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"funder":[{"name":"NSF","award":["CNS-0834260"],"award-info":[{"award-number":["CNS-0834260"]}]},{"name":"NSF","award":["CMMI-0928776"],"award-info":[{"award-number":["CMMI-0928776"]}]},{"name":"ARO","award":["W911NF-09-1-0088"],"award-info":[{"award-number":["W911NF-09-1-0088"]}]},{"DOI":"10.13039\/100000181","name":"AFOSR","doi-asserted-by":"crossref","award":["FA9550-09-1-0209"],"award-info":[{"award-number":["FA9550-09-1-0209"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"crossref"}]},{"name":"ONR","award":["ONR MURI N00014-09-1051"],"award-info":[{"award-number":["ONR MURI N00014-09-1051"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Automat. Contr."],"published-print":{"date-parts":[[2015,8]]},"DOI":"10.1109\/tac.2015.2398883","type":"journal-article","created":{"date-parts":[[2015,2,2]],"date-time":"2015-02-02T15:20:36Z","timestamp":1422890436000},"page":"2031-2045","source":"Crossref","is-referenced-by-count":102,"title":["Formal Verification and Synthesis for Discrete-Time Stochastic Systems"],"prefix":"10.1109","volume":"60","author":[{"given":"Morteza","family":"Lahijanian","sequence":"first","affiliation":[]},{"given":"Sean B.","family":"Andersson","sequence":"additional","affiliation":[]},{"given":"Calin","family":"Belta","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2007.12.002"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2008.4586912"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2013.01.004"},{"key":"ref32","first-page":"302","article-title":"Model-checking $\\omega$-regular properties of interval Markov chains","author":"chatterjee","year":"0","journal-title":"Proc Theor Prac Soft Conf Found Soft Sci Compu Str"},{"key":"ref31","first-page":"394","article-title":"Model-checking Markov chains in the presence of uncertainties","author":"sen","year":"0","journal-title":"Proc Int Conf Tools Alg Const Anal Sys"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.03.007"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1991.151651"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.3166\/EJC.18.572-587"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2011.17"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-010-0097-6"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(00)00047-3"},{"key":"ref40","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/3-540-44804-7_3","article-title":"Reachability analysis of probabilistic systems by successive refinements","volume":"2165","author":"d'argenio","year":"2001","journal-title":"Process Algebra and Probabilistic Methods Performance Modelling and Verification"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.3166\/ejc.16.624-641"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2011.2172150"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2009.5400629"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1063\/1.3129843"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78929-1_1"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2011.2160595"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2011.16"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_13"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_40"},{"key":"ref28","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1007\/11691617_5","article-title":"Don't know in probabilistic systems","author":"fecher","year":"2006","journal-title":"Model Checking Software"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2007.914952"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/2461328.2461372"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2006.886494"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2010.2072530"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_37"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/5.871304"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/s11155-005-5940-x"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"ref2","author":"clarke","year":"1999","journal-title":"Model checking"},{"key":"ref9","doi-asserted-by":"crossref","first-page":"1314","DOI":"10.1016\/j.ijar.2009.06.007","article-title":"Discrete time Markov chains with interval probabilities","volume":"50","author":"\u0161kulj","year":"2009","journal-title":"Int J Approximate Reasoning"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2012.6426184"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.09.013"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2009.2019791"},{"key":"ref21","first-page":"336","article-title":"An algorithm for quantitative verification of probabilistic transition systems","author":"van breugel","year":"2001","journal-title":"Concurrency Theory"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2009.11"},{"key":"ref23","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/s10009-004-0140-2","article-title":"Probabilistic symbolic model checking with PRISM: A hybrid approach","volume":"6","author":"kwiatkowska","year":"2004","journal-title":"Int J Softw Tools Technol Transfer (STTT)"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/1967701.1967715"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2011.6161122"}],"container-title":["IEEE Transactions on Automatic Control"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9\/7166373\/07029024.pdf?arnumber=7029024","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T11:52:05Z","timestamp":1641988325000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7029024\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,8]]},"references-count":40,"journal-issue":{"issue":"8"},"URL":"https:\/\/doi.org\/10.1109\/tac.2015.2398883","relation":{},"ISSN":["0018-9286","1558-2523"],"issn-type":[{"value":"0018-9286","type":"print"},{"value":"1558-2523","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,8]]}}}