{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T20:19:55Z","timestamp":1740169195875,"version":"3.37.3"},"reference-count":42,"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\/501100002261","name":"RFBR","doi-asserted-by":"publisher","award":["19-37-51066"],"award-info":[{"award-number":["19-37-51066"]}],"id":[{"id":"10.13039\/501100002261","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Access"],"published-print":{"date-parts":[[2020]]},"DOI":"10.1109\/access.2020.3037780","type":"journal-article","created":{"date-parts":[[2020,11,12]],"date-time":"2020-11-12T21:16:33Z","timestamp":1605215793000},"page":"207485-207498","source":"Crossref","is-referenced-by-count":2,"title":["SAT-Based Counterexample-Guided Inductive Synthesis of Distributed Controllers"],"prefix":"10.1109","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4636-2379","authenticated-orcid":false,"given":"Konstantin","family":"Chukharev","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7107-7289","authenticated-orcid":false,"given":"Dmitrii","family":"Suvorov","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6417-6254","authenticated-orcid":false,"given":"Daniil","family":"Chivilikhin","sequence":"additional","affiliation":[]},{"given":"Valeriy","family":"Vyatkin","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref39","first-page":"608","author":"holzmann","year":"2004","journal-title":"The SPIN Model Checker Primer and Reference Manual"},{"key":"ref38","first-page":"108","article-title":"Efficient CNF encoding of Boolean cardinality constraints","author":"bailleux","year":"2003","journal-title":"Principles and Practice of Constraint Programming"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-13338-6_7"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1145\/1168919.1168907"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/FSCS.1990.89597"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0249-7"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-13435-8_12"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"ref35","first-page":"441","article-title":"SAT ? CSP","author":"walsh","year":"2000","journal-title":"Proc 6th Int Conf Princ Pract Constraint Program"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/s11219-018-9429-3"},{"key":"ref10","doi-asserted-by":"crossref","first-page":"611","DOI":"10.1007\/978-3-319-15579-1_48","article-title":"BFS-based symmetry breaking predicates for DFA identification","author":"ulyantsev","year":"2015","journal-title":"Language and Automata Theory and Applications"},{"journal-title":"Distributed Algorithms","year":"1996","author":"lynch","key":"ref40"},{"key":"ref11","first-page":"291","article-title":"Learning Moore machines from input-output traces","author":"giantamidis","year":"2019","journal-title":"Formal Methods"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-95582-7_6"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_36"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-77313-1_14"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(78)90562-4"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/3061640.3061652"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2017.2670146"},{"key":"ref18","article-title":"FbSAT: Automatic inference of minimal finite-state models of function blocks using SAT solver","author":"chukharev","year":"0","journal-title":"arXiv 1907 03285"},{"journal-title":"fbSAT","year":"2020","key":"ref19"},{"key":"ref28","first-page":"980","volume":"185","author":"biere","year":"2009","journal-title":"Handbook of Satisfiability"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-015-9367-7"},{"key":"ref27","first-page":"131","article-title":"Conflict-driven clause learning SAT solvers","volume":"185","author":"marques-silva","year":"2009","journal-title":"Handbook of Satisfiability"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2008.35"},{"journal-title":"Programmable Controllers Part 1 General Information","year":"2003","key":"ref6"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050046"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2011.2166785"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_17"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15488-1_7"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.1491"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-016-0442-1"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2009.28"},{"key":"ref20","first-page":"862","author":"kurose","year":"2009","journal-title":"Computer Networking A Top-down Approach"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2020.2992235"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/INDIN.2006.275709"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1109\/IECON.2017.8216942"},{"key":"ref24","first-page":"330","author":"clarke","year":"1999","journal-title":"Model checking"},{"key":"ref41","first-page":"502","article-title":"An extensible SAT-solver","author":"e\u00e9n","year":"2003","journal-title":"Theory and Applications of Satisfiability Testing"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"ref26","first-page":"265","article-title":"Universal sequential search problems","volume":"9","author":"levin","year":"1973","journal-title":"Problems Inf Transmiss"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"}],"container-title":["IEEE Access"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6287639\/8948470\/09257351.pdf?arnumber=9257351","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,12]],"date-time":"2023-10-12T06:21:52Z","timestamp":1697091712000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9257351\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"references-count":42,"URL":"https:\/\/doi.org\/10.1109\/access.2020.3037780","relation":{},"ISSN":["2169-3536"],"issn-type":[{"type":"electronic","value":"2169-3536"}],"subject":[],"published":{"date-parts":[[2020]]}}}