Paper Info
Title
Complete Abstractions for Checking Language Inclusion
Abstract
AbstractWe study the language inclusion problem L1 ⊆ L2, where L1 is regular or context-free. Our approach relies on abstract interpretation and checks whether an overapproximating abstraction of L1, obtained by approximating the Kleene iterates of its least fixpoint characterization, is included in L2. 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 “greater than or equal to” 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.
Year
DOI
Venue
2019
10.1145/3462673
ACM Transactions on Computational Logic
Keywords
DocType
Volume
Abstract interpretation, completeness, language inclusion, regular language, context-free language, one-counter net, automaton, grammar
Journal
22
Issue
ISSN
Citations 
4
1529-3785
0
PageRank 
References 
Authors
0.34
0
3
Name
Order
Citations
PageRank
Pierre Ganty124220.29
Francesco Ranzato271141.42
Pedro Valero301.01