Wreath Products of Forest Algebras, with Applications to Tree Logics

TL;DR

This paper applies forest algebra theory to characterize tree languages definable in various logics, providing new proofs of non-definability and necessary conditions for definability.

Contribution

It introduces algebraic characterizations of unranked tree languages in different logics using forest algebra theory, advancing the understanding of logical definability.

Findings

Algebraic characterizations for CTL, EF, and first-order logic over trees.

Necessary conditions for language definability in these logics.

New proofs of non-definability for certain tree languages.

Abstract

We use the recently developed theory of forest algebras to find algebraic characterizations of the languages of unranked trees and forests definable in various logics. These include the temporal logics CTL and EF, and first-order logic over the ancestor relation. While the characterizations are in general non-effective, we are able to use them to formulate necessary conditions for definability and provide new proofs that a number of languages are not definable in these logics.