{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:35:16Z","timestamp":1770287716023,"version":"3.49.0"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2021,9,8]],"date-time":"2021-09-08T00:00:00Z","timestamp":1631059200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Spanish Ministry of Economy and Competitiveness Project","award":["PGC2018-102210-B-I00"],"award-info":[{"award-number":["PGC2018-102210-B-I00"]}]},{"name":"Madrid Regional Government Project","award":["S2018\/TCS-4339"],"award-info":[{"award-number":["S2018\/TCS-4339"]}]},{"name":"Ram\u00f3n y Cajal Fellowship","award":["RYC-2016-20281"],"award-info":[{"award-number":["RYC-2016-20281"]}]},{"name":"University of Padova, under the SID2018 project Analysis of STatic Analyses"},{"name":"Italian Ministry of Research MIUR, under the PRIN2017 Project AnalysiS of PRogram Analyses","award":["201784YSZ5"],"award-info":[{"award-number":["201784YSZ5"]}]},{"name":"Facebook Inc. under the Probability and Programming Research Award Adversarial Machine Learning by Morphological Abstract Interpretation"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2021,10,31]]},"abstract":"<jats:p>\n            We study the language inclusion problem\n            <jats:italic>L<\/jats:italic>\n            <jats:sub>1<\/jats:sub>\n            \u2286\n            <jats:italic>L<\/jats:italic>\n            <jats:sub>2<\/jats:sub>\n            , where\n            <jats:italic>L<\/jats:italic>\n            <jats:sub>1<\/jats:sub>\n            is regular or context-free. Our approach relies on abstract interpretation and checks whether an overapproximating abstraction of\n            <jats:italic>L<\/jats:italic>\n            <jats:sub>1<\/jats:sub>\n            , obtained by approximating the Kleene iterates of its least fixpoint characterization, is included in\n            <jats:italic>L<\/jats:italic>\n            <jats:sub>2<\/jats:sub>\n            . We show that a language inclusion problem is decidable whenever this overapproximating abstraction satisfies a completeness condition (i.e., its loss of precision causes no false alarm) and prevents infinite ascending chains (i.e., it guarantees termination of least fixpoint computations). This overapproximating abstraction of languages can be defined using quasiorder relations on words, where the abstraction gives the language of all the words \u201cgreater than or equal to\u201d a given input word for that quasiorder. We put forward a range of such quasiorders that allow us to systematically design decision procedures for different language inclusion problems, such as regular languages into regular languages or into trace sets of one-counter nets, and context-free languages into regular languages. In the case of inclusion between regular languages, some of the induced inclusion checking procedures correspond to well-known state-of-the-art algorithms, like the so-called antichain algorithms. Finally, we provide an equivalent language inclusion checking algorithm based on a greatest fixpoint computation that relies on quotients of languages and, to the best of our knowledge, was not previously known.\n          <\/jats:p>","DOI":"10.1145\/3462673","type":"journal-article","created":{"date-parts":[[2021,9,8]],"date-time":"2021-09-08T19:02:44Z","timestamp":1631127764000},"page":"1-40","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Complete Abstractions for Checking Language Inclusion"],"prefix":"10.1145","volume":"22","author":[{"given":"Pierre","family":"Ganty","sequence":"first","affiliation":[{"name":"IMDEA Software Institute, Madrid, Spain"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0159-0068","authenticated-orcid":false,"given":"Francesco","family":"Ranzato","sequence":"additional","affiliation":[{"name":"Dipartimento di Matematica, University of Padova, Via Trieste, Padova, Italy"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7531-6374","authenticated-orcid":false,"given":"Pedro","family":"Valero","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Madrid, Spain"}]}],"member":"320","published-online":{"date-parts":[[2021,9,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/788018.788796"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_14"},{"key":"e_1_2_1_3_1","volume-title":"Implementation and Application of Automata","author":"Almeida Andr\u00e9","unstructured":"Andr\u00e9 Almeida , Marco Almeida , Jos\u00e9 Alves , Nelma Moreira , and Rog\u00e9rio Reis . 2009. FAdo and GUItar: Tools for automata manipulation and visualization . In Implementation and Application of Automata . Springer , Berlin , 65\u201374. https:\/\/doi.org\/10.1007\/978-3-642-02979-0_10 10.1007\/978-3-642-02979-0_10 Andr\u00e9 Almeida, Marco Almeida, Jos\u00e9 Alves, Nelma Moreira, and Rog\u00e9rio Reis. 2009. FAdo and GUItar: Tools for automata manipulation and visualization. In Implementation and Application of Automata. Springer, Berlin, 65\u201374. https:\/\/doi.org\/10.1007\/978-3-642-02979-0_10"},{"key":"e_1_2_1_4_1","volume-title":"A syntactic congruence for rational \u03c9-languages. Theor. Comput. Sci. 39 (Jan","author":"Arnold Andr\u00e9","year":"1985","unstructured":"Andr\u00e9 Arnold . 1985. A syntactic congruence for rational \u03c9-languages. Theor. Comput. Sci. 39 (Jan . 1985 ), 333\u2013335. https:\/\/doi.org\/10.1016\/0304-3975(85)90148-3 10.1016\/0304-3975(85)90148-3 Andr\u00e9 Arnold. 1985. A syntactic congruence for rational \u03c9-languages. Theor. Comput. Sci. 39 (Jan. 1985), 333\u2013335. https:\/\/doi.org\/10.1016\/0304-3975(85)90148-3"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/1373322"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/1102008"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209169"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480359.2429124"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(59)90362-6"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/3264692"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/645847.668649"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01213206"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/2408037"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_5"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90124-4"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-018-0331-z"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32304-2_8"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/647170.718288"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333989"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/321127.321132"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.26"},{"key":"e_1_2_1_25_1","volume-title":"Trace inclusion for one-counter nets revisited. Theor. Comput. Sci. 735 (July","author":"Hofman Piotr","year":"2018","unstructured":"Piotr Hofman and Patrick Totzke . 2018. Trace inclusion for one-counter nets revisited. Theor. Comput. Sci. 735 (July 2018 ), 50\u201363. https:\/\/doi.org\/10.1016\/j.tcs.2017.05.009 10.1016\/j.tcs.2017.05.009 Piotr Hofman and Patrick Totzke. 2018. Trace inclusion for one-counter nets revisited. Theor. Comput. Sci. 735 (July 2018), 50\u201363. https:\/\/doi.org\/10.1016\/j.tcs.2017.05.009"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603127"},{"key":"e_1_2_1_27_1","volume-title":"Networked Systems","author":"Hol\u00edk Luk\u00e1\u0161","unstructured":"Luk\u00e1\u0161 Hol\u00edk and Roland Meyer . 2015. Antichains for the verification of recursive programs . In Networked Systems . Springer International Publishing , 322\u2013336. https:\/\/doi.org\/10.1007\/978-3-319-26850-7_22 10.1007\/978-3-319-26850-7_22 Luk\u00e1\u0161 Hol\u00edk and Roland Meyer. 2015. Antichains for the verification of recursive programs. In Networked Systems. Springer International Publishing, 322\u2013336. https:\/\/doi.org\/10.1007\/978-3-319-26850-7_22"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/1177300"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(76)80038-4"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1999.1643"},{"key":"e_1_2_1_31_1","first-page":"170","article-title":"On the Myhill-Nerod theorem for trees","volume":"47","author":"Kozen Dexter","year":"1992","unstructured":"Dexter Kozen . 1992 . On the Myhill-Nerod theorem for trees . Bull. EATCS 47 (1992), 170 \u2013 173 . Dexter Kozen. 1992. On the Myhill-Nerod theorem for trees. Bull. EATCS 47 (1992), 170\u2013173.","journal-title":"Bull. EATCS"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000034"},{"key":"e_1_2_1_33_1","volume-title":"Fixpoint induction and proofs of program properties. Mach. Intell. 5","author":"Park David","year":"1969","unstructured":"David Park . 1969. Fixpoint induction and proofs of program properties. Mach. Intell. 5 ( 1969 ). David Park. 1969. Fixpoint induction and proofs of program properties. Mach. Intell. 5 (1969)."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_3"},{"key":"e_1_2_1_35_1","volume-title":"Introduction to Static Analysis: An Abstract Interpretation Perspective","author":"Rival Xavier","unstructured":"Xavier Rival and Kwangkeun Yi. 2020. Introduction to Static Analysis: An Abstract Interpretation Perspective . MIT Press . Xavier Rival and Kwangkeun Yi. 2020. Introduction to Static Analysis: An Abstract Interpretation Perspective. MIT Press."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/1629683"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(63)90306-1"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/2601940"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3462673","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3462673","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:19:02Z","timestamp":1750191542000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3462673"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9,8]]},"references-count":38,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2021,10,31]]}},"alternative-id":["10.1145\/3462673"],"URL":"https:\/\/doi.org\/10.1145\/3462673","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,9,8]]},"assertion":[{"value":"2020-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-09-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}