Coinductive Algorithms for Büchi Automata

Issue title: Developments in Language Theory (DLT 2019)

Guest editors: Michał Skrzypczak and Piotr Hofman

Article type: Research Article

Authors: Kuperberg, Denis^{; *} | Pinault, Laureline | Pous, Damien

Affiliations: CNRS, ENS de Lyon, UCB Lyon 1, LIP, France. [email protected], [email protected], [email protected]

Correspondence: [*] Address for correspondence: CNRS, ENS de Lyon, UCB Lyon 1, LIP, France

Abstract: We propose a new algorithm for checking language equivalence of non-deterministic Büchi automata. We start from a construction proposed by Calbrix, Nivat and Podelski, which makes it possible to reduce the problem to that of checking equivalence of automata on finite words. Although this construction generates large and highly non-deterministic automata, we show how to exploit their specific structure and apply state-of-the art techniques based on coinduction to reduce the state-space that has to be explored. Doing so, we obtain algorithms which do not require full determinisation or complementation.

Keywords: Büchi automata, Language equivalence, Coinduction

DOI: 10.3233/FI-2021-2046

Journal: Fundamenta Informaticae, vol. 180, no. 4, pp. 351-373, 2021