Characterizing EF and EX tree logics

The expressive power of temporal branching time logics that use the modalities EX and EF is described. Forbidden pattern characterizations are given for tree languages definable in three logics: EX, EF and EX+EF. The characterizations give algorithms for the definability problem in the respective logics that are polynomial in the size of a deterministic tree automaton representing the language.