22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007)
Two-way unary temporal logic over trees
Wroclaw, Poland
July 10-July 14
ISBN: 0-7695-2908-9
We consider a temporal logic EF + F^-1 for unranked, unordered finite trees. The logic has two operators: EF_\varphi , which says "in some proper descendant \varphi holds", and F^-1 \varphi , which says "in some proper ancestor \varphi 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.