Forest algebra for infinite forests

I will talk about an extension of forest algebra for ω-forests. We show how the standard algebraic notions (free object, syntactic algebra, morphisms, etc) extend to the infinite case. To prove its usefulness, I will use the framework to get an effective characterization of the ω-forest languages that are definable in the temporal logic that uses the operator EF (exists finally).