  We examine languages of unranked forests definable using the temporal
operators EF and EX. We characterize the languages definable in this logic, and
various fragments thereof, using the syntactic forest algebras introduced by
Bojanczyk and Walukiewicz. Our algebraic characterizations yield efficient
algorithms for deciding when a given language of forests is definable in this
logic. The proofs are based on understanding the wreath product closures of a
few small algebras, for which we introduce a general ideal theory for forest
algebras. This combines ideas from the work of Bojanczyk and Walukiewicz for
the analogous logics on binary trees and from early work of Stiffler on wreath
product of finite semigroups.
