February 23, 2021
Kyveli Doveri
We present a novel algorithmic framework to decide whether inclusion holds between ω-regular languages of infinite words over a finite alphabet. Our approach relies on a least fixpoint characterization of languages based on ultimately periodic infinite words of type uvω, with u finite prefix and v finite period of the word. Our inclusion checking algorithm, called BAInc, is designed as a complete abstract interpretation that performs a least fixpoint computation on a suitable abstraction of sets of finite words. This abstraction is canonically defined through a pair of well-quasiorder relations on finite prefixes and periods of words. We implemented BAInc in Java as a tool called BAIT. We experimentally evaluated BAIT on an extensive suite of benchmarks and performed a comparison with state-of-the-art language inclusion checking tools. The experimental results show that BAIT advances the state-of-the-art of language inclusion tools.