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 phi holds", and F(-1)phi, 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.
temporal logic forest algebra tree automata