{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:37:21Z","timestamp":1781239041113,"version":"3.54.1"},"reference-count":132,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/501100012166","name":"National Key Fundamental Research and Development Plans","doi-asserted-by":"publisher","award":["2014CB744903"],"award-info":[{"award-number":["2014CB744903"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Aviation Science Foundation of China","award":["20150652008"],"award-info":[{"award-number":["20150652008"]}]},{"name":"Aviation Science Foundation of China","award":["20185152035"],"award-info":[{"award-number":["20185152035"]}]},{"DOI":"10.13039\/501100012226","name":"Fundamental Research Funds for the Central Universities","doi-asserted-by":"publisher","award":["NZ2013306"],"award-info":[{"award-number":["NZ2013306"]}],"id":[{"id":"10.13039\/501100012226","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61303022"],"award-info":[{"award-number":["61303022"]}],"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":["61572253"],"award-info":[{"award-number":["61572253"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Foundation","award":["61400020404"],"award-info":[{"award-number":["61400020404"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Access"],"published-print":{"date-parts":[[2020]]},"DOI":"10.1109\/access.2020.3000907","type":"journal-article","created":{"date-parts":[[2020,6,8]],"date-time":"2020-06-08T21:26:21Z","timestamp":1591651581000},"page":"108561-108578","source":"Crossref","is-referenced-by-count":14,"title":["Survey on Learning-Based Formal Methods: Taxonomy, Applications and Possible Future Directions"],"prefix":"10.1109","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9902-3859","authenticated-orcid":false,"given":"Fujun","family":"Wang","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zining","family":"Cao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lixing","family":"Tan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hui","family":"Zong","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2008.63"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368096"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_31"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1080\/00207179.2018.1458158"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2016.7799279"},{"key":"ref30","article-title":"Formal methods paradigms for estimation and machine learning in dynamical systems","author":"jones","year":"2015"},{"key":"ref37","article-title":"Foundations of active automata learning: An algorithmic perspective","author":"isberner","year":"2015"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1145\/2967606"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45923-5_6"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31984-9_14"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2019.2924639"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-018-0316-7"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/3380625.3380659"},{"key":"ref20","article-title":"Identification of timed behavior models for diagnosis in production systems","author":"maier","year":"2015"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/2728606.2728628"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/11817949_29"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2010.24"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2014.7039363"},{"key":"ref101","doi-asserted-by":"publisher","DOI":"10.1109\/SWCT.1964.8"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/2907943"},{"key":"ref100","doi-asserted-by":"publisher","DOI":"10.1007\/s10994-016-5565-9"},{"key":"ref25","article-title":"On learning assumptions for compositional verification of probabilistic systems","author":"feng","year":"2013"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8603016"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10512-3_3"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1145\/2562059.2562146"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2014.7039487"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90110-9"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04244-7_26"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34691-0_11"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-019-00332-1"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-67531-2_13"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29860-8_12"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.3923\/itj.2012.1391.1399"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74792-5_6"},{"key":"ref3","author":"clarke","year":"1999","journal-title":"Model checking"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96562-8_5"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21455-4_8"},{"key":"ref8","article-title":"ML + FV $= \\heartsuit$ ? A survey on the application of machine learning to formal verification","author":"amrani","year":"2018","journal-title":"arxiv 1806 03600"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1145\/3316781.3317847"},{"key":"ref7","first-page":"3","volume":"11026","author":"bennaceur","year":"2018","journal-title":"Machine Learning for Software Analysis Models Methods and Applications"},{"key":"ref9","article-title":"Model learning: A survey on foundation, tools and applications","author":"ali","year":"2018","journal-title":"arXiv 1901 01910"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-017-0447-4"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2015.2421907"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99154-2_20"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.23919\/ECC.2018.8550271"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_30"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1972.5009015"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250749"},{"key":"ref43","article-title":"Generating effective test suites for reactive systems using specification mining","author":"bokil","year":"2014"},{"key":"ref127","doi-asserted-by":"publisher","DOI":"10.1109\/INFOCT.2019.8711369"},{"key":"ref126","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03542-0_20"},{"key":"ref125","doi-asserted-by":"publisher","DOI":"10.1145\/1837274.1837466"},{"key":"ref124","article-title":"An empirical study on practicality of specification mining algorithms on a real-world application","author":"jafar mashhadi","year":"2019","journal-title":"arXiv 1903 11242"},{"key":"ref73","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181808"},{"key":"ref72","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503275"},{"key":"ref129","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781316823187","author":"jacobs","year":"2016","journal-title":"Introduction to coalgebra Towards mathematics of states and observations"},{"key":"ref71","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040314"},{"key":"ref128","doi-asserted-by":"publisher","DOI":"10.1007\/1-4020-4223-X"},{"key":"ref70","doi-asserted-by":"publisher","DOI":"10.1007\/BF00993306"},{"key":"ref76","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.103.6"},{"key":"ref130","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511792588.003"},{"key":"ref77","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2011.21"},{"key":"ref74","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11164-3_26"},{"key":"ref75","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_14"},{"key":"ref131","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06880-0_20"},{"key":"ref78","first-page":"1004","article-title":"Angluin-style learning of NFA","author":"bollig","year":"2009","journal-title":"Proc IJCAI"},{"key":"ref132","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-72056-2_5"},{"key":"ref79","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_51"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1145\/2883817.2883843"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1145\/377978.377990"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-45231-8_30"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0086"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"ref65","first-page":"1907","article-title":"Model checking: Theories, techniques and applications","volume":"30","author":"huimin","year":"2002","journal-title":"Acta Electronica Sinica"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_34"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_21"},{"key":"ref68","doi-asserted-by":"publisher","DOI":"10.2514\/6.2019-0682"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8"},{"key":"ref69","first-page":"1","article-title":"Robust satisfaction of temporal logic specifications via reinforcement learning","author":"jones","year":"2015","journal-title":"Proc CDC"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3540-6"},{"key":"ref109","author":"hangos","year":"2001","journal-title":"Process Modelling and Model Analysis"},{"key":"ref95","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2010.5530540"},{"key":"ref108","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-68612-7"},{"key":"ref94","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00982-2_63"},{"key":"ref107","first-page":"205","article-title":"Prevent: A predictive run-time verification framework using statistical learning","author":"babaee","year":"2018","journal-title":"Proc SEFM"},{"key":"ref93","doi-asserted-by":"publisher","DOI":"10.1142\/9789812797919_0007"},{"key":"ref106","first-page":"23","article-title":"On the identification of $\\alpha$ -asynchronous cellular automata in the case of partial observations with spatially separated gaps","author":"bo?t","year":"2016","journal-title":"Challenging Problems and Solutions in Intelligent Systems"},{"key":"ref92","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139194655"},{"key":"ref105","doi-asserted-by":"publisher","DOI":"10.1109\/CEC.2015.7257258"},{"key":"ref91","first-page":"363","article-title":"Anomaly detection in production plants using timed automata","author":"maier","year":"2011","journal-title":"Proc ICINCO"},{"key":"ref104","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzl007"},{"key":"ref90","doi-asserted-by":"publisher","DOI":"10.1109\/INDIN.2014.6945484"},{"key":"ref103","first-page":"225","article-title":"Black box checking","volume":"7","author":"peled","year":"2002","journal-title":"J Automata Lang Combinat"},{"key":"ref102","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1021"},{"key":"ref111","article-title":"Lecture notes on hybrid systems","author":"lygeros","year":"2006"},{"key":"ref112","doi-asserted-by":"publisher","DOI":"10.1109\/ICMLA.2012.158"},{"key":"ref110","doi-asserted-by":"publisher","DOI":"10.1007\/0-8176-4404-0_5"},{"key":"ref98","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03769-7_11"},{"key":"ref99","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2018.2886898"},{"key":"ref96","doi-asserted-by":"publisher","DOI":"10.1080\/00207721.2011.649369"},{"key":"ref97","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-25945-1_10"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-75632-5_5"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03769-7_4"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(87)90052-6"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58473-0_144"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2016.01.004"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360251"},{"key":"ref118","first-page":"1","author":"bowman","year":"2006","journal-title":"Concurrency Theory"},{"key":"ref16","author":"hopcroft","year":"2001","journal-title":"Introduction to Automata Theory Languages and Computation"},{"key":"ref82","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2011-607"},{"key":"ref117","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(95)00016-6"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008330914786"},{"key":"ref81","doi-asserted-by":"publisher","DOI":"10.5772\/48398"},{"key":"ref18","author":"baier","year":"2008","journal-title":"Principles of Model Checking"},{"key":"ref84","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(67)91165-5"},{"key":"ref119","doi-asserted-by":"publisher","DOI":"10.1002\/tee.21728"},{"key":"ref19","article-title":"Identifying behavior models for hybrid production systems","author":"voden?arevi?","year":"2013"},{"key":"ref83","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(78)90562-4"},{"key":"ref114","doi-asserted-by":"publisher","DOI":"10.1109\/ETFA.2011.6059080"},{"key":"ref113","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2004.1348029"},{"key":"ref116","doi-asserted-by":"publisher","DOI":"10.1109\/ICAT.2011.6102093"},{"key":"ref80","first-page":"31","article-title":"Learning minimal separating DFA’s for compositional verification","author":"chen","year":"2009","journal-title":"Proc TACAS"},{"key":"ref115","doi-asserted-by":"publisher","DOI":"10.1109\/INDIN.2012.6301128"},{"key":"ref120","doi-asserted-by":"publisher","DOI":"10.1016\/j.biosystems.2005.06.002"},{"key":"ref89","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30206-3_26"},{"key":"ref121","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11936-6_8"},{"key":"ref122","doi-asserted-by":"publisher","DOI":"10.1016\/j.mejo.2011.11.003"},{"key":"ref123","doi-asserted-by":"publisher","DOI":"10.1109\/CDC40024.2019.9029181"},{"key":"ref85","doi-asserted-by":"publisher","DOI":"10.1145\/1968.1972"},{"key":"ref86","article-title":"Active learning: Theory and applications","author":"tong","year":"2001"},{"key":"ref87","first-page":"975","article-title":"Probabilistic DFA inference using Kullback-Leibler divergence and minimality","author":"thollard","year":"2000","journal-title":"Proc ICML"},{"key":"ref88","article-title":"Efficient identification of timed automata: Theory and practice","author":"verwer","year":"2010"}],"container-title":["IEEE Access"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6287639\/8948470\/09110834.pdf?arnumber=9110834","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,27]],"date-time":"2022-10-27T05:28:30Z","timestamp":1666848510000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9110834\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"references-count":132,"URL":"https:\/\/doi.org\/10.1109\/access.2020.3000907","relation":{},"ISSN":["2169-3536"],"issn-type":[{"value":"2169-3536","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]}}}