Deciding Inclusion for Languages of Infinite Words

February 23, 2021

Kyveli Doveri


Deciding Inclusion for Languages of Infinite Words

Time:   11:00am
Location:   Zoom3 - https://zoom.us/j/3911012202 (pass: s3)

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.