Ultimately periodic words of rational ω-languages

In this paper we initiate the following program: Associate sets of finite words to Büchi-recognizable sets of infinite words, and reduce algorithmic problems on Büchi automata to simpler ones on automata on finite words. We know that the set of ultimately periodic words UP(L) of a rational language of infinite words L is sufficient to characterize L, since UP(L₁)=UP(L₂) implies L₁=L₂. We can use this fact as a test, for example, of the equivalence of two given Büchi automata. The main technical result in this paper is the construction of an automaton which recognizes the set of all finite words u · $ · v which naturally represent the ultimately periodic words of the form u ·554-01 in the language of infinite words recognized by a given Büchi automaton.