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.
展开▼
