Inclusion Checking Algorithms for ω-Languages

We consider the inclusion problem for ω-languages. In particular we are interested in the cases such as the inclusion between two ω-regular languages or the inclusion problem of ω-context free languages into ω-regular languages. We built on an abstract interpretation based framework solving the inclusion problem for languages of finite words [Ganty et al. , SAS, 2019] that was first presented at Highlights’18. Our approach can be summarised in two parts: first the reduction of the inclusion problem to an inclusion between the ultimate periodic subsets of the languages we consider. The ultimately periodic subset of an ω-language L is the subset of L containing all the words of the form uv^ω, where u and v are finite words referred to as the prefix and period, respectively. The advantage is that it admits a least fixed point characterisation. Second, the definition of abstractions build upon pairs of quasiorders on finite words that we derive from the language we want to check inclusion into. Intuitively, the first quasiorder of such a pair is used to reason on the prefixes of words uv^ω while the second one is used to reason on the periods. We obtain complete abstract interpretations, from which we derive sound and complete algorithms to decide the inclusion. This is joint work with Pierre Ganty.

Authors

• Kyveli Doveri

Keywords

No keywords are indexed for this paper.