When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2021.3
URN: urn:nbn:de:0030-drops-143802
URL: https://drops.dagstuhl.de/opus/volltexte/2021/14380/
 Go to the corresponding LIPIcs Volume Portal

### Inclusion Testing of Büchi Automata Based on Well-Quasiorders

 pdf-format:

### Abstract

We introduce an algorithmic framework to decide whether inclusion holds between languages of infinite words over a finite alphabet. Our approach falls within the class of Ramsey-based methods and relies on a least fixpoint characterization of ω-languages leveraging ultimately periodic infinite words of type uv^ω, with u a finite prefix and v a finite period of an infinite word. We put forward an inclusion checking algorithm between Büchi automata, called BAInc, designed as a complete abstract interpretation using a pair of well-quasiorders on finite words. BAInc is quite simple: it consists of two least fixpoint computations (one for prefixes and the other for periods) manipulating finite sets (of pairs) of states compared by set inclusion, so that language inclusion holds when the sets (of pairs) of states of the fixpoints satisfy some basic conditions. We implemented BAInc in a tool called BAIT that we experimentally evaluated against the state-of-the-art. We gathered, in addition to existing benchmarks, a large number of new case studies stemming from program verification and word combinatorics, thereby significantly expanding both the scope and size of the available benchmark set. Our experimental results show that BAIT advances the state-of-the-art on an overwhelming majority of these benchmarks. Finally, we demonstrate the generality of our algorithmic framework by instantiating it to the inclusion problem of Büchi pushdown automata into Büchi automata.

### BibTeX - Entry

@InProceedings{doveri_et_al:LIPIcs.CONCUR.2021.3,
author =	{Doveri, Kyveli and Ganty, Pierre and Parolini, Francesco and Ranzato, Francesco},
title =	{{Inclusion Testing of B\"{u}chi Automata Based on Well-Quasiorders}},
booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages =	{3:1--3:22},
series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN =	{978-3-95977-203-7},
ISSN =	{1868-8969},
year =	{2021},
volume =	{203},
publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/14380},
URN =		{urn:nbn:de:0030-drops-143802},
doi =		{10.4230/LIPIcs.CONCUR.2021.3},
annote =	{Keywords: B\"{u}chi (Pushdown) Automata, \omega-Language Inclusion, Well-quasiorders}
}

 Keywords: Büchi (Pushdown) Automata, ω-Language Inclusion, Well-quasiorders Collection: 32nd International Conference on Concurrency Theory (CONCUR 2021) Issue Date: 2021 Date of publication: 13.08.2021 Supplementary Material: Software (Source Code): https://github.com/parof/bait archived at: https://archive.softwareheritage.org/swh:1:dir:0085d9456cf1300c44386339a996c9453dca17c2

DROPS-Home | Fulltext Search | Imprint | Privacy