IMDEA Software

IMDEA initiative

Home > Events > Software Seminar Series > 2021 > Deciding Inclusion for Languages of Infinite Words

Kyveli Doveri

Tuesday, February 23, 2021

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

Kyveli Doveri, PhD Student, IMDEA Software Institute

Deciding Inclusion for Languages of Infinite Words

Abstract:

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.