@inproceedings{10.1007/978-3-031-30823-9_15,
    Abstract = {We define novel algorithms for the inclusion problem between two visibly pushdown languages of infinite words, an EXPTime-complete problem. Our algorithms search for counterexamples to inclusion in the form of ultimately periodic words i.e. words of the form {\$}{\$}uv^{\{}{\backslash}omega {\}}{\$}{\$}uv$\omega$where {\$}{\$}u{\$}{\$}uand {\$}{\$}v{\$}{\$}vare finite words. They are parameterized by a pair of quasiorders telling which ultimately periodic words need not be tested as counterexamples to inclusion without compromising completeness. The pair of quasiorders enables distinct reasoning for prefixes and periods of ultimately periodic words thereby allowing to discard even more words compared to using the same quasiorder for both. We put forward two families of quasiorders: the state-based quasiorders based on automata and the syntactic quasiorders based on languages. We also implemented our algorithm and conducted an empirical evaluation on benchmarks from software verification.},
    Address = {Cham},
    Author = {Doveri, Kyveli and Ganty, Pierre and Had{\v{z}}i-{\DJ}oki{\'{c}}, Luka},
    BookTitle = {Tools and Algorithms for the Construction and Analysis of Systems},
    Editor = {Sankaranarayanan, Sriram and Sharygina, Natasha},
    File = {Antichains Algorithms for the Inclusion Problem Between 𝜔-VPL - 978-3-031-30823-9\_15.pdf},
    ISBN = {978-3-031-30823-9},
    Pages = {290--307},
    Publisher = {Springer Nature Switzerland},
    Title = {Antichains Algorithms for the Inclusion Problem Between omega-VPL},
    Year = {2023},
    date-added = {2023-04-28 16:07:56 +0200},
    date-modified = {2023-04-28 16:07:56 +0200},
    doi = {10.1007/978-3-031-30823-9_15}
}

@inproceedings{10.1007/978-3-031-30823-9_15, Abstract = {We define novel algorithms for the inclusion problem between two visibly pushdown languages of infinite words, an EXPTime-complete problem. Our algorithms search for counterexamples to inclusion in the form of ultimately periodic words i.e. words of the form {\$}{\$}uv^{{}{\backslash}omega {}}{\$}{\$}uv$\omega$where {\$}{\$}u{\$}{\$}uand {\$}{\$}v{\$}{\$}vare finite words. They are parameterized by a pair of quasiorders telling which ultimately periodic words need not be tested as counterexamples to inclusion without compromising completeness. The pair of quasiorders enables distinct reasoning for prefixes and periods of ultimately periodic words thereby allowing to discard even more words compared to using the same quasiorder for both. We put forward two families of quasiorders: the state-based quasiorders based on automata and the syntactic quasiorders based on languages. We also implemented our algorithm and conducted an empirical evaluation on benchmarks from software verification.}, Address = {Cham}, Author = {Doveri, Kyveli and Ganty, Pierre and Had{\v{z}}i-{\DJ}oki{\'{c}}, Luka}, BookTitle = {Tools and Algorithms for the Construction and Analysis of Systems}, Editor = {Sankaranarayanan, Sriram and Sharygina, Natasha}, File = {Antichains Algorithms for the Inclusion Problem Between 𝜔-VPL - 978-3-031-30823-9_15.pdf}, ISBN = {978-3-031-30823-9}, Pages = {290--307}, Publisher = {Springer Nature Switzerland}, Title = {Antichains Algorithms for the Inclusion Problem Between omega-VPL}, Year = {2023}, date-added = {2023-04-28 16:07:56 +0200}, date-modified = {2023-04-28 16:07:56 +0200}, doi = {10.1007/978-3-031-30823-9_15} }