{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T15:07:13Z","timestamp":1775315233461,"version":"3.50.1"},"reference-count":59,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"1","license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61772347"],"award-info":[{"award-number":["61772347"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100017380","name":"Science and Technology Foundation of Shenzhen City","doi-asserted-by":"publisher","award":["JCYJ20170302153712968"],"award-info":[{"award-number":["JCYJ20170302153712968"]}],"id":[{"id":"10.13039\/100017380","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IIEEE Trans. Software Eng."],"published-print":{"date-parts":[[2021,1,1]]},"DOI":"10.1109\/tse.2018.2886898","type":"journal-article","created":{"date-parts":[[2018,12,14]],"date-time":"2018-12-14T17:29:42Z","timestamp":1544808582000},"page":"189-203","source":"Crossref","is-referenced-by-count":4,"title":["Automatically \u2018Verifying\u2019 Discrete-Time Complex Systems through Learning, Abstraction and Refinement"],"prefix":"10.1109","volume":"47","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7113-7635","authenticated-orcid":false,"given":"Jingyi","family":"Wang","sequence":"first","affiliation":[]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3028-8191","authenticated-orcid":false,"given":"Shengchao","family":"Qin","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2770-8394","authenticated-orcid":false,"given":"Cyrille","family":"Jegourel","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16612-9_11"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87785-1_5"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66335-7_23"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_16"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1145\/565816.503279"},{"key":"ref37","article-title":"PRISM DTMC benchmark models","author":"kwiatkowska","year":"0"},{"key":"ref36","first-page":"203","article-title":"The PRISM benchmark suite","author":"kwiatkowska","year":"2012","journal-title":"Proc 9th Int Conf Quantitative Eval Syst"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30482-1_23"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45790-9_12"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46002-0_24"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/982962.964021"},{"key":"ref2","year":"0"},{"key":"ref1","year":"0"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/BF00994018"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1137\/120871456"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139194655"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2017.01.037"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_10"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_8"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1137\/16M1079397"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_16"},{"key":"ref51","first-page":"276","article-title":"Runtime monitoring of stochastic cyber-physical systems with hybrid state","author":"sistla","year":"2011","journal-title":"Proc Int'l Conf Runtime Verification"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2014.2351652"},{"key":"ref58","article-title":"Verification and planning for stochastic processes with asynchronous events","author":"younes","year":"2005"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_17"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19829-8_10"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54494-5_1"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2007.10"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2016.11.006"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-11(3:8)2015"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45187-7_32"},{"key":"ref11","volume":"26202649","author":"baier","year":"2008","journal-title":"Principles of Model Checking"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2011.21"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11936-6_8"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58473-0_144"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1051\/ita:1999102"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/1961189.1961199"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_22"},{"key":"ref17","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1007\/10722167_15","article-title":"Counterexample-guided abstraction refinement","author":"clarke","year":"2000","journal-title":"Proc Int Conf Comput Aided Verification"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24372-1_1"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/3127041.3131362"},{"key":"ref3","year":"0"},{"key":"ref6","first-page":"931","article-title":"Java-ML: A machine learning library","volume":"10","author":"abeel","year":"2009","journal-title":"Journal of Machine Learning Research"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_12"},{"key":"ref8","article-title":"Identifying languages from stochastic examples","author":"angluin","year":"1988"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(87)90052-6"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2004.1348029"},{"key":"ref9","author":"wald","year":"1947","journal-title":"Sequential Analysis"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40465-8_8"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1145\/290163.290168"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1023\/A:1026490906255"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1145\/225298.225302"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.103.6"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1007\/s10994-016-5565-9"},{"key":"ref44","first-page":"722","article-title":"Model-based testing","author":"pretschner","year":"2005","journal-title":"Proc 27th Int l Conf Software Eng"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11164-3_28"}],"container-title":["IEEE Transactions on Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/32\/9318455\/08576657.pdf?arnumber=8576657","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T14:11:28Z","timestamp":1775311888000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8576657\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,1]]},"references-count":59,"journal-issue":{"issue":"1"},"URL":"https:\/\/doi.org\/10.1109\/tse.2018.2886898","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":[[2021,1,1]]}}}