Two-Way Unary Temporal Logic over Trees

We consider a temporal logic EF+F^-1 for unranked, unordered finite trees.The logic has two operators: EF\phi, which says "in some proper descendant \phiholds", and F^-1\phi, which says "in some proper ancestor \phi holds". Wepresent an algorithm for deciding if a regular language of unranked finitetrees can be expressed in EF+F^-1. The algorithm uses a characterizationexpressed in terms of forest algebras.Comment: 29 pages. Journal version of a LICS 07 pape