Two-Way Unary Temporal Logic over Trees

TL;DR

This paper introduces a decision procedure for a specific temporal logic over unranked, unordered finite trees, enabling the characterization of regular tree languages expressible in this logic.

Contribution

It provides a novel algorithm based on forest algebras to determine if a regular tree language can be expressed in EF+F^-1 logic.

Findings

Algorithm for deciding expressibility in EF+F^-1

Characterization of tree languages using forest algebras

Decidability results for temporal logic over trees

Abstract

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.