{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:16:26Z","timestamp":1784837786309,"version":"3.55.0"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031131875","type":"print"},{"value":"9783031131882","type":"electronic"}],"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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T00:00:00Z","timestamp":1659744000000},"content-version":"vor","delay-in-days":217,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>\n\nWe propose a novel algorithm to decide the language inclusion between (nondeterministic) B\u00fcchi automata, a <jats:sc>PSpace<\/jats:sc>-complete problem. Our approach, like others before, leverage a notion of quasiorder to prune the search for a counterexample by discarding candidates which are subsumed by others for the quasiorder. Discarded candidates are guaranteed to not compromise the completeness of the algorithm. The novelty of our work lies in the quasiorder used to discard candidates. We introduce FORQs (family of right quasiorders) that we obtain by adapting the notion of family of right congruences put forward by Maler and Staiger in 1993. We define a FORQ-based inclusion algorithm which we prove correct and instantiate it for a specific FORQ, called the structural FORQ, induced by the B\u00fcchi automaton to the right of the inclusion sign. The resulting implementation, called <jats:sc>Forklift<\/jats:sc>, scales up better than the state-of-the-art on a variety of benchmarks including benchmarks from program verification and theorem proving for word combinatorics. <jats:bold>Artifact:<\/jats:bold><jats:ext-link xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" ext-link-type=\"uri\" xlink:href=\"https:\/\/doi.org\/10.5281\/zenodo.6552870\">https:\/\/doi.org\/10.5281\/zenodo.6552870<\/jats:ext-link><\/jats:p>","DOI":"10.1007\/978-3-031-13188-2_6","type":"book-chapter","created":{"date-parts":[[2022,8,5]],"date-time":"2022-08-05T08:16:57Z","timestamp":1659687417000},"page":"109-129","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["FORQ-Based Language Inclusion Formal Testing"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9403-2860","authenticated-orcid":false,"given":"Kyveli","family":"Doveri","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3625-6003","authenticated-orcid":false,"given":"Pierre","family":"Ganty","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6425-5369","authenticated-orcid":false,"given":"Nicolas","family":"Mazzocchi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,8,6]]},"reference":[{"key":"6_CR1","unstructured":"BAIT: an $$\\omega $$-regular language inclusion checker. https:\/\/github.com\/parof\/bait. Accessed 17 Jan 2022"},{"key":"6_CR2","unstructured":"FORKLIFT: FORQ-based language inclusion formal testing. https:\/\/github.com\/Mazzocchi\/FORKLIFT. Accessed 7 Jun 2022"},{"key":"6_CR3","unstructured":"GOAL: graphical tool for omega-automata and logics. http:\/\/goal.im.ntu.edu.tw\/wiki\/doku.php. Accessed 17 Jan 2022"},{"key":"6_CR4","unstructured":"RABIT\/Reduce: tools for language inclusion testing and reduction of nondeterministic B\u00fcchi automata and NFA. http:\/\/www.languageinclusion.org\/doku.php?id=tools. Accessed 17 Jan 2022"},{"key":"6_CR5","unstructured":"ROLL library: Regular Omega Language Learning library. https:\/\/github.com\/ISCAS-PMC\/roll-library. Accessed 17 Jan 2022"},{"key":"6_CR6","unstructured":"Spot: a platform for LTL and $$\\omega $$-automata manipulation. https:\/\/spot.lrde.epita.fr\/. Accessed 17 Jan 2022"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-642-14295-6_14","volume-title":"Computer Aided Verification","author":"PA Abdulla","year":"2010","unstructured":"Abdulla, P.A.: Simulation subsumption in Ramsey-based B\u00fcchi automata universality and inclusion testing. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 132\u2013147. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_14"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-23217-6_13","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"PA Abdulla","year":"2011","unstructured":"Abdulla, P.A.: Advanced Ramsey-based B\u00fcchi automata inclusion testing. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 187\u2013202. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-23217-6_13"},{"key":"6_CR9","doi-asserted-by":"publisher","unstructured":"Angluin, D., Boker, U., Fisman, D.: Families of DFAs as acceptors of $$\\omega $$-regular languages. Log. Meth. Comput. Sci. 14 (2018). https:\/\/doi.org\/10.23638\/LMCS-14(1:15)2018","DOI":"10.23638\/LMCS-14(1:15)2018"},{"key":"6_CR10","doi-asserted-by":"publisher","unstructured":"Clemente, L., Mayr, R.: Efficient reduction of nondeterministic automata with application to language inclusion testing. Log. Meth. Comput. Sci. 15(1) (2019). https:\/\/doi.org\/10.23638\/LMCS-15(1:12)2019","DOI":"10.23638\/LMCS-15(1:12)2019"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/11817963_5","volume-title":"Computer Aided Verification","author":"M De Wulf","year":"2006","unstructured":"De Wulf, M., Doyen, L., Henzinger, T.A., Raskin, J.-F.: Antichains: a new algorithm for checking universality of finite automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 17\u201330. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_5"},{"key":"6_CR12","unstructured":"Doveri, K., Ganty, P., Parolini, F., Ranzato, F.: B\u00fcchi automata benchmarks for language inclusion (2021). https:\/\/github.com\/parof\/buchi-automata-benchmark"},{"key":"6_CR13","doi-asserted-by":"publisher","unstructured":"Doveri, K., Ganty, P., Parolini, F., Ranzato, F.: Inclusion testing of B\u00fcchi automata based on well-quasiorders. In: 32nd International Conference on Concurrency Theory (CONCUR). LIPIcs (2021). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2021.3","DOI":"10.4230\/LIPIcs.CONCUR.2021.3"},{"key":"6_CR14","doi-asserted-by":"publisher","unstructured":"Doyen, L., Raskin, J.F.: Antichains for the automata-based approach to model-checking. Log. Meth. Comput. Sci. 5(1) (2009). https:\/\/doi.org\/10.2168\/lmcs-5(1:5)2009","DOI":"10.2168\/lmcs-5(1:5)2009"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-319-46520-3_8","volume-title":"Automated Technology for Verification and Analysis","author":"A Duret-Lutz","year":"2016","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, \u00c9., Xu, L.: Spot 2.0\u2014a framework for LTL and $$\\omega $$-automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 122\u2013129. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_8"},{"key":"6_CR16","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., et al.: From spot 2.0 to spot 2.10: what\u2019s new? In: Shoham, S., Vizel, Y. (eds.) CAV 2022. LNCS, vol. 13372, pp. xx\u2013yy (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_18","DOI":"10.1007\/978-3-031-13188-2_18"},{"key":"6_CR17","unstructured":"Esparza, J.: Automata Theory - An Algorithmic Approach. Lecture Notes (2017). https:\/\/www7.in.tum.de\/~esparza\/autoskript.pdf"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/978-3-642-12002-2_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Fogarty","year":"2010","unstructured":"Fogarty, S., Vardi, M.Y.: Efficient B\u00fcchi universality checking. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 205\u2013220. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_17"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/978-3-319-89963-3_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Heizmann","year":"2018","unstructured":"Heizmann, M.: Ultimate automizer and the search for perfect interpolants. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 447\u2013451. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_30"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-642-39799-8_2","volume-title":"Computer Aided Verification","author":"M Heizmann","year":"2013","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36\u201352. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_2"},{"key":"6_CR21","doi-asserted-by":"publisher","unstructured":"Hieronymi, P., Ma, D., Oei, R., Schaeffer, L., Schulz, C., Shallit, J.: Decidability for Sturmian words. In: 30th EACSL Annual Conference on Computer Science Logic (CSL). LIPIcs (2022). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2022.24","DOI":"10.4230\/LIPIcs.CSL.2022.24"},{"key":"6_CR22","doi-asserted-by":"publisher","unstructured":"Kuperberg, D., Pinault, L., Pous, D.: Coinductive algorithms for B\u00fcchi automata. Fundam. Informaticae 180(4) (2021). https:\/\/doi.org\/10.3233\/FI-2021-2046","DOI":"10.3233\/FI-2021-2046"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/3-540-61474-5_84","volume-title":"Computer Aided Verification","author":"O Kupferman","year":"1996","unstructured":"Kupferman, O., Vardi, M.Y.: Verification of fair transition systems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 372\u2013382. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61474-5_84"},{"key":"6_CR24","doi-asserted-by":"publisher","first-page":"104678","DOI":"10.1016\/j.ic.2020.104678","volume":"281","author":"Y Li","year":"2020","unstructured":"Li, Y., Chen, Y.F., Zhang, L., Liu, D.: A novel learning algorithm for B\u00fcchi automata based on family of DFAs and classification trees. Inf. Comput. 281, 104678 (2020). https:\/\/doi.org\/10.1016\/j.ic.2020.104678","journal-title":"Inf. Comput."},{"key":"6_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-030-17462-0_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Li","year":"2019","unstructured":"Li, Y., Sun, X., Turrini, A., Chen, Y.-F., Xu, J.: ROLL 1.0: $$\\omega $$-regular language learning library. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 365\u2013371. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_23"},{"key":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/978-3-030-90870-6_25","volume-title":"Formal Methods","author":"Y Li","year":"2021","unstructured":"Li, Y., Tsay, Y.-K., Turrini, A., Vardi, M.Y., Zhang, L.: Congruence relations for b\u00fcchi automata. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 465\u2013482. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_25"},{"key":"6_CR27","doi-asserted-by":"publisher","unstructured":"de Luca, A., Varricchio, S.: Well quasi-orders and regular languages. Acta Informatica 31(6) (1994). https:\/\/doi.org\/10.1007\/BF01213206","DOI":"10.1007\/BF01213206"},{"key":"6_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"586","DOI":"10.1007\/3-540-56503-5_58","volume-title":"STACS 93","author":"O Maler","year":"1993","unstructured":"Maler, O., Staiger, L.: On syntactic congruences for \u03c9\u2014languages. In: Enjalbert, P., Finkel, A., Wagner, K.W. (eds.) STACS 1993. LNCS, vol. 665, pp. 586\u2013594. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56503-5_58"},{"key":"6_CR29","doi-asserted-by":"publisher","unstructured":"Maler, O., Staiger, L.: On syntactic congruences for $$\\omega $$-languages. Theor. Comput. Sci. 183(1) (1997). https:\/\/doi.org\/10.1016\/S0304-3975(96)00312-X","DOI":"10.1016\/S0304-3975(96)00312-X"},{"key":"6_CR30","unstructured":"Maler, O., Staiger, L.: On syntactic congruences for $$\\omega $$-languages. Technical report, Verimag, France (2008). http:\/\/www-verimag.imag.fr\/~maler\/Papers\/congr.pdf"},{"key":"6_CR31","unstructured":"Oei, R., Ma, D., Schulz, C., Hieronymi, P.: Pecan: an automated theorem prover for automatic sequences using B\u00fcchi automata. CoRR abs\/2102.01727 (2021). https:\/\/arxiv.org\/abs\/2102.01727"},{"key":"6_CR32","doi-asserted-by":"publisher","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. Log. Meth. Comput. Sci. 3(3) (2007). https:\/\/doi.org\/10.2168\/lmcs-3(3:5)2007","DOI":"10.2168\/lmcs-3(3:5)2007"},{"key":"6_CR33","doi-asserted-by":"publisher","unstructured":"Tsai, M., Fogarty, S., Vardi, M.Y., Tsay, Y.: State of B\u00fcchi complementation. Log. Meth. Comput. Sci. 10(4) (2014). https:\/\/doi.org\/10.2168\/LMCS-10(4:13)2014","DOI":"10.2168\/LMCS-10(4:13)2014"},{"key":"6_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"883","DOI":"10.1007\/978-3-642-39799-8_62","volume-title":"Computer Aided Verification","author":"M-H Tsai","year":"2013","unstructured":"Tsai, M.-H., Tsay, Y.-K., Hwang, Y.-S.: GOAL for games, omega-automata, and logics. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 883\u2013889. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_62"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-13188-2_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,5]],"date-time":"2022-08-05T08:17:32Z","timestamp":1659687452000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-13188-2_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031131875","9783031131882"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-13188-2_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"6 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","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":"7 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"209","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":"40","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":"11","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":"19% - 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.9","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":"9.7","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)"}}]}}