A Uniform Framework for Language Inclusion Problems
Kyveli Doveri, Pierre Ganty, Chana Weil-Kennedy
TL;DR
The paper gives a unified, fixpoint-based framework for language inclusion problems that avoids explicit complementation by using a least fixpoint characterization of the smaller language and a well-behaved quasiorder on words to guarantee finite convergence. By instantiating the framework with a state-based quasiorder derived from automata, it derives practical algorithms (including antichain variants and saturation-based methods) for CFGs into REG and related cases, with termination guaranteed by the monotone, M-preserving, decidable well-quasiorder. It then extends the approach to a variety of inclusion problems, including REG ⊆ REG, REG ⊆ Petri net traces, and ω-regular languages, and discusses further directions such as VPL and operator-precedence languages. The work emphasizes algorithmic efficiency (e.g., antichains, context-based updates, and SLP saturation data-structures) and broad applicability to static analysis, model checking, and compressed text processing. Overall, the framework provides a scalable, modular method to decide language inclusion across several language classes by reducing the problem to a finite set of membership checks in the larger language using fixpoint theory and well-quasiorders.
Abstract
We present a uniform approach for solving language inclusion problems. Our approach relies on a least fixpoint characterization and a quasiorder to compare words of the "smaller" language, reducing the inclusion check to a finite number of membership queries in the "larger" language. We present our approach in detail on the case of inclusion of a context-free language given by a grammar into a regular language. We then explore other inclusion problems and discuss how to apply our approach.