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: EFphi , which says "in some proper descendant phi holds", and F^-1phi , which says "in some proper ancestor phi holds". We present an algorithm for deciding if a regular language of unranked finite trees can be expressed in EF + F^-1. The algorithm uses a characterization expressed in terms of forest algebras.