Algebra for infinite forests with an application to the temporal logic ef

Abstract

We define 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, we 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). © 2009 Springer Berlin Heidelberg.