Two-Way Unary Temporal Logic over Trees
arXiv:0904.4119 · doi:10.2168/LMCS-5(3:5)2009
Abstract
We consider a temporal logic EF+F^-1 for unranked, unordered finite trees. The logic has two operators: EFϕ, which says "in some proper descendant ϕholds", and F^-1ϕ, which says "in some proper ancestor ϕ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.
29 pages. Journal version of a LICS 07 paper