Unambiguous Büchi Automata

by Olivier Carton and Max Michel


Résumé

Dans cet article, nous introduisons une classe particulière d'automates de Büchi appelés non ambigus. Dans ces automates, tout mot infini est l'étiquette d'exactement un seul chemin qui passe infiniment par des états finaux. Le mot est accepté par l'automate si ce chemin commence à un état initial. Le résultat principal est que tout ensemble rationnel de mots infinis est reconnu par un tel automate. Nous donnons deux preuves de ce résultats. Nous donnons également quelques résultats connexes.

Abstract

In this paper, we introduce a special class of Büchi automata called unambiguous. In these automata, any infinite word labels exactly one path going infinitely often through final states. The word is accepted by the automaton if this path starts at an initial state. The main result of the paper is that any rational set of infinite words is recognized by such an automaton. We also provide two characterizations of these automata. We finally show that they are well suitable for boolean operations.


PDF Files