On the expressive power of temporal logic for infinite words (Q805240)

The paper gives a self-contained algebraic proof of the equivalence between propositional temporal logic and star-free languages of infinite words. The equivalence is known, but the previous proof was indirectly obtained by establishing first the equivalence with the first-order logic. The present proof is based on a theorem of Schützenberger, which characterizes the \(\omega\)-star-free languages in terms of prefix codes.