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 characterization 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. Starting from the celebrated Schutzenberger theorem [12], characterizing star-...

• Type: Conference
• Year: 2004
• Where: CONCUR
• Authors: Mikolaj Bojanczyk, Igor Walukiewicz
• Keywords: CONCUR 2004, Definability Problem, Expressive Power, Tree