{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T09:31:48Z","timestamp":1777541508267,"version":"3.51.4"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030888848","type":"print"},{"value":"9783030888855","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-88885-5_4","type":"book-chapter","created":{"date-parts":[[2021,10,13]],"date-time":"2021-10-13T17:25:06Z","timestamp":1634145906000},"page":"48-64","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Certifying DFA Bounds for Recognition and Separation"],"prefix":"10.1007","author":[{"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":[[2021,10,12]]},"reference":[{"key":"4_CR1","unstructured":"Almagor, S., Lahijanian, M.: Explainable multi agent path finding. In: Proceedings of 19th AAMAS, pp. 34\u201342 (2020)"},{"key":"4_CR2","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B Alpern","year":"1987","unstructured":"Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2, 117\u2013126 (1987)","journal-title":"Distrib. Comput."},{"issue":"2","key":"4_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.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87\u2013106 (1987)","journal-title":"Inf. Comput."},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-030-59152-6_23","volume-title":"Automated Technology for Verification and Analysis","author":"T Baumeister","year":"2020","unstructured":"Baumeister, T., Finkbeiner, B., Torfah, H.: Explainable reactive synthesis. In: Hung, D.V., Sokolsky, O. (eds.) ATVA 2020. LNCS, vol. 12302, pp. 413\u2013428. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_23"},{"key":"4_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, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. AMS 138, 295\u2013311 (1969)","journal-title":"Trans. AMS"},{"key":"4_CR6","unstructured":"Czerwi\u0144ski, W., Lasota, S., Meyer, R., Muskalla, S., Kumar, K.N., Saivasan, P.: Regular separability of well-structured transition systems. In: Proceedings of 29th CONCUR. LIPIcs, vol. 118, pp. 35:1\u201335:18 (2018)"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-642-39212-2_16","volume-title":"Automata, Languages, and Programming","author":"W Czerwi\u0144ski","year":"2013","unstructured":"Czerwi\u0144ski, W., Martens, W., Masopust, T.: Efficient separability of regular languages by subsequences and suffixes. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013. LNCS, vol. 7966, pp. 150\u2013161. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39212-2_16"},{"key":"4_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.: Inferring regular languages and $$\\omega $$-languages. J. Log. Algebraic Methods Program. 98, 27\u201349 (2018)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-319-68167-2_5","volume-title":"Automated Technology for Verification and Analysis","author":"G Gange","year":"2017","unstructured":"Gange, G., Ganty, P., Stuckey, P.J.: Fixing the state budget: approximation of regular languages with small DFAs. In: D\u2019Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 67\u201383. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_5"},{"issue":"3","key":"4_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, E.M.: Complexity of automaton identification from given data. Inf. Control 37(3), 302\u2013320 (1978)","journal-title":"Inf. Control"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-642-15488-1_7","volume-title":"Grammatical Inference: Theoretical Results and Applications","author":"MJH Heule","year":"2010","unstructured":"Heule, M.J.H., Verwer, S.: Exact DFA identification using SAT solvers. In: Sempere, J.M., Garc\u00eda, P. (eds.) ICGI 2010. LNCS (LNAI), vol. 6339, pp. 66\u201379. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15488-1_7"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-030-71995-1_20","volume-title":"Foundations of Software Science and Computation Structures","author":"O Kupferman","year":"2021","unstructured":"Kupferman, O., Sickert, S.: Certifying inexpressibility. In: FOSSACS 2021. LNCS, vol. 12650, pp. 385\u2013405. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-71995-1_20"},{"key":"4_CR13","unstructured":"Kupferman, O., Lavee, N., Sickert, S.: Certifying DFA bounds for recognition and separation (2021). Full version archived at arXiv:2107.01566"},{"issue":"3","key":"4_CR14","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods Syst. Des. 19(3), 291\u2013314 (2001)","journal-title":"Formal Methods Syst. Des."},{"key":"4_CR15","first-page":"591","volume":"305","author":"O Kupferman","year":"2005","unstructured":"Kupferman, O., Vardi, M.Y.: From complementation to certification. Theoret. Comput. Sci. 305, 591\u2013606 (2005)","journal-title":"Theoret. Comput. Sci."},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-642-39611-3_22","volume-title":"Hardware and Software: Verification and Testing","author":"O Kupferman","year":"2013","unstructured":"Kupferman, O., Weiner, S.: Environment-friendly safety. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 227\u2013242. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39611-3_22"},{"key":"4_CR17","unstructured":"Myhill, J.: Finite automata and the representation of events. Technical report WADD TR-57-624, pp. 112\u2013137. Wright Patterson AFB, Ohio (1957)"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-642-33386-6_28","volume-title":"Automated Technology for Verification and Analysis","author":"D Neider","year":"2012","unstructured":"Neider, D.: Computing minimal separating DFAs and regular invariants using SAT and SMT solvers. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 354\u2013369. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33386-6_28"},{"issue":"4","key":"4_CR19","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.: Linear automaton transformations. Proc. Am. Math. Soc. 9(4), 541\u2013544 (1958)","journal-title":"Proc. Am. Math. Soc."},{"issue":"12","key":"4_CR20","doi-asserted-by":"publisher","first-page":"1099","DOI":"10.1109\/T-C.1973.223655","volume":"22","author":"CP Pfleeger","year":"1973","unstructured":"Pfleeger, C.P.: State reduction in incompletely specified finite-state machines. IEEE Trans. Comput. 22(12), 1099\u20131102 (1973)","journal-title":"IEEE Trans. Comput."},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"T. Place and M. Zeitoun. Separating regular languages with first-order logic. Log. Methods Comput. Sci. 12(1) (2016)","DOI":"10.2168\/LMCS-12(1:5)2016"},{"key":"4_CR22","unstructured":"ESF Network Programme: Automata: from mathematics to applications (AutoMathA) (2010). http:\/\/www.esf.org\/index.php?id=1789"},{"key":"4_CR23","unstructured":"Almagor, S., Chistikov, D., Ouaknine, J., Worrell, J.: O-minimal invariants for linear loops. In: Proceedings of 45th ICALP. LIPIcs, vol. 107, pp. 114:1\u2013114:14 (2018)"},{"key":"4_CR24","unstructured":"Schewe, S.: Beyond hyper-minimisation\u2013minimising DBAs and DPAs is NP-complete. In: Proceedings of 30th FST & TCS. LIPIcs, vol. 8, pp. 400\u2013411 (2010)"},{"key":"4_CR25","volume-title":"Finite Automata","author":"BA Trakhtenbrot","year":"1973","unstructured":"Trakhtenbrot, B.A., Barzdin, Y.M.: Finite Automata. North Holland, Amsterdam (1973)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-88885-5_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,13]],"date-time":"2021-10-13T17:51:22Z","timestamp":1634147482000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-88885-5_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030888848","9783030888855"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-88885-5_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"12 October 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Gold Coast, QLD","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Australia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 October 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 October 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/formal-analysis.com\/atva\/2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"75","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"25% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"In addition there are 4 tool papers. The conference was held online because of the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}