{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T12:48:04Z","timestamp":1740142084456,"version":"3.37.3"},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2022,3,15]],"date-time":"2022-03-15T00:00:00Z","timestamp":1647302400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,3,15]],"date-time":"2022-03-15T00:00:00Z","timestamp":1647302400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["436811179"],"award-info":[{"award-number":["436811179"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003977","name":"Israel Science Foundation","doi-asserted-by":"crossref","award":["2357\/192357\/19"],"award-info":[{"award-number":["2357\/192357\/19"]}],"id":[{"id":"10.13039\/501100003977","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2022,9]]},"DOI":"10.1007\/s11334-022-00446-6","type":"journal-article","created":{"date-parts":[[2022,3,15]],"date-time":"2022-03-15T20:04:40Z","timestamp":1647374680000},"page":"405-416","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Certifying DFA Bounds for Recognition and Separation"],"prefix":"10.1007","volume":"18","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4699-6117","authenticated-orcid":false,"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nir","family":"Lavee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Salomon","family":"Sickert","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,3,15]]},"reference":[{"key":"446_CR1","unstructured":"Almagor S, Lahijanian M (2020) Explainable multi agent path finding. In Proceedings of the 19th international conference on autonomous agents and multiagent systems, pp 34\u201342"},{"key":"446_CR2","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B Alpern","year":"1987","unstructured":"Alpern B, Schneider FB (1987) Recognizing safety and liveness. Distrib Comput 2:117\u2013126","journal-title":"Distrib Comput"},{"issue":"2","key":"446_CR3","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D Angluin","year":"1987","unstructured":"Angluin D (1987) Learning regular sets from queries and counter examples. Inf Comput 75(2):87\u2013106","journal-title":"Inf Comput"},{"key":"446_CR4","doi-asserted-by":"crossref","unstructured":"Baumeister T, Finkbeiner B, Torfah H (2020) Explainable reactive synthesis","DOI":"10.1007\/978-3-030-59152-6_23"},{"key":"446_CR5","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1090\/S0002-9947-1969-0280205-0","volume":"138","author":"JR B\u00fcchi","year":"1969","unstructured":"B\u00fcchi JR, Landweber LH (1969) Solving sequential conditions by finite-state strategies. Trans AMS 138:295\u2013311","journal-title":"Trans AMS"},{"key":"446_CR6","unstructured":"Czerwinski W, Lasota S, Meyer R, Muskalla S, Kumar KN, Saivasan P (2018) Regular separability of well-structured transition systems. In: Proceedings of the 29th International Conference on Concurrency Theory, volume 118 of LIPIcs, pp 35:1\u201335:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik"},{"key":"446_CR7","doi-asserted-by":"crossref","unstructured":"Czerwinski W, Martens W, Masopust T (2013) Efficient separability of regular languages by subsequences and suffixes. In: Proceedings 40th International Colloqege on Automata, Languages, and Programming, volume 7966 of Lecture Notes in Computer Science, pp 150\u2013161. Springer","DOI":"10.1007\/978-3-642-39212-2_16"},{"key":"446_CR8","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/j.jlamp.2018.03.002","volume":"98","author":"D Fisman","year":"2018","unstructured":"Fisman D (2018) Inferring regular languages and $$\\omega $$-languages. J Log Algebraic Methods Program 98:27\u201349","journal-title":"J Log Algebraic Methods Program"},{"key":"446_CR9","doi-asserted-by":"crossref","unstructured":"Gange G, Ganty P, Stuckey PJ (2017) Fixing the state budget: approximation of regular languages with small dfas. In: 15th International symposium on automated technology for verification and analysis, volume 10482 of Lecture Notes in Computer Science, pp 67\u201383. Springer","DOI":"10.1007\/978-3-319-68167-2_5"},{"issue":"3","key":"446_CR10","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1016\/S0019-9958(78)90562-4","volume":"37","author":"EM Gold","year":"1978","unstructured":"Gold EM (1978) Complexity of automaton identification from given data. Inf Control 37(3):302\u2013320","journal-title":"Inf Control"},{"key":"446_CR11","doi-asserted-by":"crossref","unstructured":"Heule M, Verwer S (2010) Exact DFA identification using SAT solvers. In: Grammatical inference: theoretical results and applications, 10th international colloquium, volume 6339 of Lecture Notes in Computer Science, pp 66\u201379. Springer","DOI":"10.1007\/978-3-642-15488-1_7"},{"key":"446_CR12","doi-asserted-by":"crossref","unstructured":"Kupferman O, Sickert S (2021) Certifying inexpressibility. In: Proceedings of the 24th international conference on foundations of software science and computation structures, volume 12650 of Lecture Notes in Computer Science, pp 385\u2013405. Springer","DOI":"10.1007\/978-3-030-71995-1_20"},{"issue":"3","key":"446_CR13","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman O, Vardi MY (2001) Model checking of safety properties. Formal Methods Syst Des 19(3):291\u2013314","journal-title":"Formal Methods Syst Des"},{"key":"446_CR14","first-page":"591","volume":"305","author":"O Kupferman","year":"2005","unstructured":"Kupferman O, Vardi MY (2005) From complementation to certification. Theor Comput Sci 305:591\u2013606","journal-title":"Theor Comput Sci"},{"key":"446_CR15","doi-asserted-by":"crossref","unstructured":"Kupferman O, Weiner S (2012) Environment-friendly safety. In: 8th International Haifa verification conference, volume 7857 of Lecture Notes in Computer Science, pp 227\u2013242. Springer","DOI":"10.1007\/978-3-642-39611-3_22"},{"key":"446_CR16","unstructured":"Myhill J (1957) Finite automata and the representation of events. Technical Report WADD TR-57-624, pp 112\u2013137, Wright Patterson AFB, Ohio"},{"key":"446_CR17","doi-asserted-by":"crossref","unstructured":"Neider D (2012) Computing minimal separating dfas and regular invariants using SAT and SMT solvers. In: 10th International symposium on automated technology for verification and analysis, volume 7561 of Lecture Notes in Computer Science, pp 354\u2013369. Springer","DOI":"10.1007\/978-3-642-33386-6_28"},{"issue":"4","key":"446_CR18","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1090\/S0002-9939-1958-0135681-9","volume":"9","author":"A Nerode","year":"1958","unstructured":"Nerode A (1958) Linear automaton transformations. Proc Am Math Soc 9(4):541\u2013544","journal-title":"Proc Am Math Soc"},{"key":"446_CR19","doi-asserted-by":"crossref","unstructured":"Pfleeger CP (1973) State reduction in incompletely specified finite-state machines. IEEE Trans Comput 22(12):1099\u20131102","DOI":"10.1109\/T-C.1973.223655"},{"key":"446_CR20","doi-asserted-by":"crossref","unstructured":"Place T, Zeitoun M (2016) Separating regular languages with first-order logic. Log Methods Comput Sci, 12(1)","DOI":"10.2168\/LMCS-12(1:5)2016"},{"key":"446_CR21","unstructured":"ESF (2010) Network programme. Automata: from mathematics to applications (AutoMathA). http:\/\/www.esf.org\/index.php?id=1789,"},{"key":"446_CR22","unstructured":"Almagor S, Chistikov D, Ouaknine J, Worrell J (2018) O-minimal invariants for linear loops. In : Proceedings of the 45th international colloqioum on automata, languages, and programming, volume 107 of LIPIcs, pp 114:1\u2013114:14. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik"},{"key":"446_CR23","unstructured":"Schewe S (2010) Beyond Hyper-Minimisation\u2014Minimising DBAs and DPAs is NP-Complete. In: Proceedings of the 30th Conference on Foundations of Software Technology and Theoretical Computer Science, volume\u00a08 of Leibniz International Proceedings in Informatics (LIPIcs), pp 400\u2013411"},{"key":"446_CR24","unstructured":"Trakhtenbrot BA, Barzdin YM (1973) Finite Automata. North Holland"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-022-00446-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11334-022-00446-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-022-00446-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,12]],"date-time":"2022-09-12T06:43:25Z","timestamp":1662965005000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11334-022-00446-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,3,15]]},"references-count":24,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2022,9]]}},"alternative-id":["446"],"URL":"https:\/\/doi.org\/10.1007\/s11334-022-00446-6","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"type":"print","value":"1614-5046"},{"type":"electronic","value":"1614-5054"}],"subject":[],"published":{"date-parts":[[2022,3,15]]},"assertion":[{"value":"24 October 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 February 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 March 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}