{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T03:14:44Z","timestamp":1776482084624,"version":"3.51.2"},"reference-count":53,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"7","license":[{"start":{"date-parts":[[2016,7,1]],"date-time":"2016-07-01T00:00:00Z","timestamp":1467331200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"funder":[{"DOI":"10.13039\/501100001459","name":"Ministry of Education - Singapore","doi-asserted-by":"publisher","award":["R-252-000-458-133"],"award-info":[{"award-number":["R-252-000-458-133"]}],"id":[{"id":"10.13039\/501100001459","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"publisher","award":["DP130102764"],"award-info":[{"award-number":["DP130102764"]}],"id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"publisher","award":["DP160101652"],"award-info":[{"award-number":["DP160101652"]}],"id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61428208"],"award-info":[{"award-number":["61428208"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61502260"],"award-info":[{"award-number":["61502260"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006296","name":"CAS\/SAFEA","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100006296","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100011246","name":"State Key Laboratory of Novel Software Technology at Nanjing University","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100011246","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IIEEE Trans. Software Eng."],"published-print":{"date-parts":[[2016,7,1]]},"DOI":"10.1109\/tse.2015.2508444","type":"journal-article","created":{"date-parts":[[2015,12,17]],"date-time":"2015-12-17T16:42:09Z","timestamp":1450370529000},"page":"623-639","source":"Crossref","is-referenced-by-count":12,"title":["Asymptotic Perturbation Bounds for Probabilistic Model Checking with Empirically Determined Probability Parameters"],"prefix":"10.1109","volume":"42","author":[{"given":"Guoxin","family":"Su","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuan","family":"Feng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Taolue","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David S.","family":"Rosenblum","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_12"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73551-9_10"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2013.01.004"},{"key":"ref32","first-page":"32","article-title":"LTL model checking of interval Markov chains","author":"benedikt","year":"0","journal-title":"Proc Int Conf Tools Algorithms Construction Anal Syst"},{"key":"ref31","first-page":"302","article-title":"Model-checking omega-regular properties of interval Markov chains","author":"chatterjee","year":"0","journal-title":"Proc Found Softw Sci Comput Struct"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-012-0277-5"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1980.234477"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2015.2421318"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1016\/S0024-3795(01)00320-2"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33512-9_10"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19835-9_30"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88562-7_20"},{"key":"ref29","article-title":"Formal verification with confidence intervals: A new approach to establishing the quality-of-service properties of software systems","author":"calinescu","year":"2015","journal-title":"IEEE Trans Rel"},{"key":"ref2","author":"norris","year":"1998","journal-title":"Markov Chains"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/2330667.2330686"},{"key":"ref20","author":"baier","year":"2008","journal-title":"Principles of Model Checking"},{"key":"ref22","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1051\/ita\/1996300100011","article-title":"Relationships among PL, #L, and the determinant","volume":"30","author":"allender","year":"1996","journal-title":"Theoretical Informatics and Applications"},{"key":"ref21","author":"mieghem","year":"2005","journal-title":"Performance Analysis of Communications Networks and Systems"},{"key":"ref24","year":"2012","journal-title":"version 8 0 (R2012b)"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1137\/0203021"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11936-6_26"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21455-4_3"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39813-4_26"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04761-9_10"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1145\/210332.210339"},{"key":"ref52","first-page":"724","article-title":"Complementation, disambiguation, and determinization of Büchi automata unified","author":"k\u00e4hler","year":"0","journal-title":"Proc 35th Int Colloq Automata Lang Programm"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985840"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1137\/S1052623400366802"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1109\/WODES.2008.4605929"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_26"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2013.20"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_35"},{"key":"ref15","author":"stewart","year":"1990","journal-title":"Matrix Perturbation Theory"},{"key":"ref16","author":"kato","year":"2005","journal-title":"Perturbation Theory for Linear Operators"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-41202-8_20"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568256"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44584-6_16"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1205180"},{"key":"ref3","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1016\/S0927-0507(05)80172-0","article-title":"Markov decision processes","volume":"2","author":"puterman","year":"1990","journal-title":"Handbooks in Operations Research and Management Science"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1985.12"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31862-0_21"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1007\/11682462_25"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0146-x"},{"key":"ref46","first-page":"203","article-title":"The PRISM benchmark suite","author":"kwiatkowska","year":"0","journal-title":"Proc 9th Int Conf Quantitative Eval Syst"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2005.852033"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_5"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1145\/2629417"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1007\/11557432_25"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606606"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31984-9_9"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606549"}],"container-title":["IEEE Transactions on Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/32\/7513344\/07355393.pdf?arnumber=7355393","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T11:46:04Z","timestamp":1641987964000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/7355393\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,7,1]]},"references-count":53,"journal-issue":{"issue":"7"},"URL":"https:\/\/doi.org\/10.1109\/tse.2015.2508444","relation":{},"ISSN":["0098-5589","1939-3520","2326-3881"],"issn-type":[{"value":"0098-5589","type":"print"},{"value":"1939-3520","type":"electronic"},{"value":"2326-3881","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,7,1]]}}}