Antichains Algorithms for the Inclusion Problem Between ω-VPL

We define novel algorithms for the inclusion problem between two ω-visibly pushdown languages, an EXPTime-complete problem. Intuitively our algorithms search for counterexamples to inclusion in the form of ultimately periodic words, that are words of the form uv^ω where u and v are finite words. The search is pruned using antichain-like techniques: a quasiorder tells us which ultimately periodic words need not be tested as counterexamples to inclusion without compromising completeness. Our algorithm uniquely combines antichain-like techniques with the use of distinct quasiorders for prefix and period of ultimately periodic words. The use of distinct quasiorders for prefix and period enables further pruning compared to a unique quasiorder for both. We put forward two families of quasiorders: the state-based quasiorders based on automata and the syntactic quasiorders based on languages. This is a joint work with Pierre Ganty and Luka Hadzi-Djokic.

Authors

• Kyveli Doveri

Keywords

No keywords are indexed for this paper.