Characterizing EF and EX tree logics

We describe the expressive power of temporal branching time logics that use the modalities EX and EF. We give a forbidden pattern char-acterization of the tree languages definable in three logics: EX, EF and EX+EF. The properties in these characterizations can be verified in polynomial time when given a minimal deterministic bottom-up tree automaton. We consider the definability problem for logics over binary trees: given a regular tree language decide if it can be expressed by a formula of the logic in question. The main motivation for considering this problem is to understand the expressive power of tree logics. Although a very old question, definability has gained new relevance with the XML community’s burgeoning interest in tree models [8]. Indeed, numerous new formalisms for describing tree properties have been recently proposed. For words the definability question is well studied and understood. Start