H. Calbrix et al., A DECISION PROCEDURE FOR THE MONADIC 2ND- ORDER LOGIC OF ONE SUCCESSOR, Comptes rendus de l'Academie des sciences. Serie 1, Mathematique, 318(9), 1994, pp. 847-850
Since they have been introduced by Richard Bachi in 1962, Bachi automa
ta recognizing sets of infinite words are basic tools of decisions pro
ofs of the monadic logic SIS and temporal logics, used in program and
circuit checking. We are showing in this Note that we can get rid of a
utomata on infinite words thanks to a finite representation of infinit
e ultimately periodic words recognized by a Bachi automaton. Moreover,
our procedure produces minimal deterministic automata.