{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T20:08:46Z","timestamp":1743019726934,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031166808"},{"type":"electronic","value":"9783031166815"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"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":[[2022]]},"DOI":"10.1007\/978-3-031-16681-5_17","type":"book-chapter","created":{"date-parts":[[2022,9,16]],"date-time":"2022-09-16T03:41:24Z","timestamp":1663299684000},"page":"241-255","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Methods for\u00a0NFA Equivalence: QBFs, Witness Extraction, and\u00a0Encoding Verification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7115-626X","authenticated-orcid":false,"given":"Edith","family":"Hemaspaandra","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3704-1060","authenticated-orcid":false,"given":"David E.","family":"Narv\u00e1ez","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,9,17]]},"reference":[{"key":"17_CR1","unstructured":"Aho, A.V., Lam, M.S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools, 2 edn. Addison Wesley (2006)"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-642-22600-7_5","volume-title":"Descriptional Complexity of Formal Systems","author":"L Alpoge","year":"2011","unstructured":"Alpoge, L., Ang, T., Schaeffer, L., Shallit, J.: Decidability and shortest strings in formal languages. In: Holzer, M., Kutrib, M., Pighizzini, G. (eds.) DCFS 2011. LNCS, vol. 6808, pp. 55\u201367. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22600-7_5"},{"key":"17_CR3","doi-asserted-by":"publisher","unstructured":"Bonchi, F., Pous, D.: Checking NFA equivalence with bisimulations up to congruence. In: Giacobazzi, R., Cousot, R. (eds.) POPL, pp. 457\u2013468. ACM (2013). https:\/\/doi.org\/10.1145\/2429069.2429124","DOI":"10.1145\/2429069.2429124"},{"issue":"2","key":"17_CR4","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1145\/2713167","volume":"58","author":"F Bonchi","year":"2015","unstructured":"Bonchi, F., Pous, D.: Hacking nondeterminism with induction and coinduction. Commun. ACM 58(2), 87\u201395 (2015). https:\/\/doi.org\/10.1145\/2713167","journal-title":"Commun. ACM"},{"key":"17_CR5","unstructured":"Brunner, J.: Transition systems and automata. Archive of Formal Proofs (2017). https:\/\/isa-afp.org\/entries\/Transition_Systems_and_Automata.html. Formal proof development"},{"issue":"3","key":"17_CR6","doi-asserted-by":"publisher","first-page":"695","DOI":"10.1007\/s10817-018-9490-4","volume":"63","author":"L Cruz-Filipe","year":"2018","unstructured":"Cruz-Filipe, L., Marques-Silva, J., Schneider-Kamp, P.: Formally verifying the solution to the Boolean Pythagorean triples problem. J. Autom. Reason. 63(3), 695\u2013722 (2018). https:\/\/doi.org\/10.1007\/s10817-018-9490-4","journal-title":"J. Autom. Reason."},{"key":"17_CR7","doi-asserted-by":"publisher","unstructured":"Goldberg, E., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: Design, Automation and Test in Europe Conference and Exhibition, pp. 886\u2013891. IEEE (2003). https:\/\/doi.org\/10.1109\/DATE.2003.1253718","DOI":"10.1109\/DATE.2003.1253718"},{"key":"17_CR8","doi-asserted-by":"publisher","unstructured":"Hecking-Harbusch, J., Tentrup, L.: Solving QBF by abstraction. In: Proceedings Ninth International Symposium on Games, Automata, Logics, and Formal Verification. Electron. Proc. Theor. Comput. Sci. (EPTCS), vol. 277, pp. 88\u2013102. EPTCS (2018). https:\/\/doi.org\/10.4204\/EPTCS.277.7","DOI":"10.4204\/EPTCS.277.7"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-319-08587-6_7","volume-title":"Automated Reasoning","author":"MJH Heule","year":"2014","unstructured":"Heule, M.J.H., Seidl, M., Biere, A.: A unified proof system for QBF preprocessing. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 91\u2013106. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_7"},{"key":"17_CR10","doi-asserted-by":"publisher","unstructured":"Heule, M.J., Hunt, W.A., Wetzler, N.: Trimming while checking clausal proofs. In: Formal Methods in Computer-Aided Design, pp. 181\u2013188. IEEE (2013). https:\/\/doi.org\/10.1109\/FMCAD.2013.6679408","DOI":"10.1109\/FMCAD.2013.6679408"},{"issue":"6","key":"17_CR11","doi-asserted-by":"publisher","first-page":"1087","DOI":"10.1142\/S0129054103002199","volume":"14","author":"M Holzer","year":"2003","unstructured":"Holzer, M., Kutrib, M.: Nondeterministic descriptional complexity of regular languages. Int. J. Found. Comput. Sci. 14(6), 1087\u20131102 (2003). https:\/\/doi.org\/10.1142\/S0129054103002199","journal-title":"Int. J. Found. Comput. Sci."},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Hopcroft, J.: An $$n \\log n$$ algorithm for minimizing states in a finite automaton. Tech. Rep. STAN-CS-71-190, Stanford University (1971)","DOI":"10.1016\/B978-0-12-417750-5.50022-1"},{"key":"17_CR13","unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley (1979)"},{"key":"17_CR14","doi-asserted-by":"publisher","unstructured":"Hoque, K.A., Mohamed, O.A., Abed, S., Boukadoum, M.: An automated sat encoding-verification approach for efficient model checking. In: 2010 International Conference on Microelectronics, pp. 419\u2013422. IEEE (2010). https:\/\/doi.org\/10.1109\/ICM.2010.5696177","DOI":"10.1109\/ICM.2010.5696177"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-319-94144-8_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2018","author":"M Janota","year":"2018","unstructured":"Janota, M.: Circuit-based search space pruning in QBF. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 187\u2013198. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94144-8_12"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Janota, M.: Towards generalization in QBF solving via machine learning. In: McIlraith, S.A., Weinberger, K.Q. (eds.) AAAI, pp. 6607\u20136614. AAAI Press (2018). http:\/\/dblp.uni-trier.de\/db\/conf\/aaai\/aaai2018.html#Janota18","DOI":"10.1609\/aaai.v32i1.12208"},{"issue":"2","key":"17_CR17","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/j.tcs.2004.04.011","volume":"330","author":"G Jir\u00e1skov\u00e1","year":"2005","unstructured":"Jir\u00e1skov\u00e1, G.: State complexity of some operations on binary regular languages. Theor. Comput. Sci. 330(2), 287\u2013298 (2005). https:\/\/doi.org\/10.1016\/j.tcs.2004.04.011","journal-title":"Theor. Comput. Sci."},{"key":"17_CR18","unstructured":"Jordan, C., Klieber, W., Seidl, M.: Non-CNF QBF solving with QCIR. In: Darwiche, A. (ed.) AAAI Workshop: Beyond NP. AAAI Workshops, vol. WS-16-05. AAAI Press (2016). http:\/\/www.aaai.org\/ocs\/index.php\/WS\/AAAIW16\/paper\/view\/12601"},{"issue":"3","key":"17_CR19","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/j.entcs.2006.12.022","volume":"174","author":"T Jussila","year":"2007","unstructured":"Jussila, T., Biere, A.: Compressing BMC encodings with QBF. Electron. Notes Theor. Comput. Sci. 174(3), 45\u201356 (2007). https:\/\/doi.org\/10.1016\/j.entcs.2006.12.022","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"17_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-540-72788-0_21","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"T Jussila","year":"2007","unstructured":"Jussila, T., Biere, A., Sinz, C., Kr\u00f6ning, D., Wintersteiger, C.M.: A first step towards a unified proof checker for QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 201\u2013214. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-72788-0_21"},{"key":"17_CR21","doi-asserted-by":"publisher","unstructured":"Meyer, A.R., Fischer, M.J.: Economy of description by automata, grammars, and formal systems. In: 12th Annual Symposium on Switching and Automata Theory, East Lansing, Michigan, USA, 13\u201315 October 1971, pp. 188\u2013191. IEEE Computer Society (1971). https:\/\/doi.org\/10.1109\/SWAT.1971.11","DOI":"10.1109\/SWAT.1971.11"},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"Miller, H., Narv\u00e1ez, D.E.: Toward determining NFA equivalence via QBFs. In: AAAI-21 Student Abstract (2021). To appear","DOI":"10.1609\/aaai.v35i18.17921"},{"issue":"10","key":"17_CR23","doi-asserted-by":"publisher","first-page":"1211","DOI":"10.1109\/T-C.1971.223108","volume":"20","author":"FR Moore","year":"1971","unstructured":"Moore, F.R.: On the bounds for state-set size in the proofs of equivalence between deterministic, nondeterministic, and two-way finite automata. IEEE Trans. Comput. 20(10), 1211\u20131214 (1971). https:\/\/doi.org\/10.1109\/T-C.1971.223108","journal-title":"IEEE Trans. Comput."},{"key":"17_CR24","unstructured":"Nipkow, T.: Boolean expression checkers. Archive of Formal Proofs (2014). https:\/\/isa-afp.org\/entries\/Boolean_Expression_Checkers.html. Formal proof development"},{"key":"17_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-319-66263-3_19","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2017","author":"T Peitl","year":"2017","unstructured":"Peitl, T., Slivovsky, F., Szeider, S.: Dependency Learning for QBF. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 298\u2013313. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66263-3_19"},{"issue":"2","key":"17_CR26","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1147\/rd.32.0114","volume":"3","author":"MO Rabin","year":"1959","unstructured":"Rabin, M.O., Scott, D.S.: Finite automata and their decision problems. IBM J. Res. Dev. 3(2), 114\u2013125 (1959). https:\/\/doi.org\/10.1147\/rd.32.0114","journal-title":"IBM J. Res. Dev."},{"key":"17_CR27","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/3-540-45653-8_25","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J Rintanen","year":"2001","unstructured":"Rintanen, J.: Partial implicit unfolding in the Davis-Putnam procedure for quantified Boolean formulae. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 362\u2013376. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45653-8_25"},{"key":"17_CR28","doi-asserted-by":"publisher","unstructured":"Rochester Institute of Technology: Research computing services (2019). https:\/\/doi.org\/10.34788\/0S3G-QD15","DOI":"10.34788\/0S3G-QD15"},{"issue":"2","key":"17_CR29","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/S0022-0000(70)80006-X","volume":"4","author":"WJ Savitch","year":"1970","unstructured":"Savitch, W.J.: Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci. 4(2), 177\u2013192 (1970). https:\/\/doi.org\/10.1016\/S0022-0000(70)80006-X","journal-title":"J. Comput. Syst. Sci."},{"key":"17_CR30","doi-asserted-by":"publisher","unstructured":"Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time (preliminary report). In: Proceedings of the Fifth Annual ACM Symposium on Theory of Computing, pp. 1\u20139. STOC 1973, ACM, New York, NY, USA (1973). https:\/\/doi.org\/10.1145\/800125.804029","DOI":"10.1145\/800125.804029"},{"key":"17_CR31","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/11591191_28","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D Tabakov","year":"2005","unstructured":"Tabakov, D., Vardi, M.Y.: Experimental evaluation of classical automata constructions. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 396\u2013411. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11591191_28"},{"key":"17_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/978-3-319-40970-2_24","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"L Tentrup","year":"2016","unstructured":"Tentrup, L.: Non-prenex QBF solving using abstraction. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 393\u2013401. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_24"},{"key":"17_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-319-09284-3_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"N Wetzler","year":"2014","unstructured":"Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422\u2013429. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_31"},{"issue":"2","key":"17_CR34","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1016\/0304-3975(92)00011-F","volume":"125","author":"S Yu","year":"1994","unstructured":"Yu, S., Zhuang, Q., Salomaa, K.: The state complexities of some basic operations on regular languages. Theor. Comput. Sci. 125(2), 315\u2013328 (1994). https:\/\/doi.org\/10.1016\/0304-3975(92)00011-F","journal-title":"Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-16681-5_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,16]],"date-time":"2022-09-16T03:43:29Z","timestamp":1663299809000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-16681-5_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031166808","9783031166815"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-16681-5_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"17 September 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tbilisi","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Georgia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 September 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 September 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2022\/cicm.php","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":"37","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":"17","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":"4","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":"46% - 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":"2.95","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.9","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":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}