  We study the language inclusion problem $L_1 \subseteq L_2$ where $L_1$ is
regular or context-free. Our approach relies on abstract interpretation and
checks whether an overapproximating abstraction of $L_1$, obtained by
overapproximating the Kleene iterates of its least fixpoint characterization,
is included in $L_2$. 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.
