Some connections between universal algebra and logics for trees

TL;DR

This paper explores the relationship between universal algebra and logical definability of regular tree languages, aiming to address the open problem of deciding first-order definability through algebraic methods.

Contribution

It introduces a novel algebraic framework to analyze the problem of characterizing regular tree languages definable in first-order logic.

Findings

Highlights potential connections to Tame Congruence Theory

Proposes an algebraic approach to logical definability

Identifies structural properties relevant to the problem

Abstract

One of the major open problems in automata and logic is the following: is there an algorithm which inputs a regular tree language and decides if the language can be defined in first-order logic? The goal of this paper is to present this problem and similar ones using the language of universal algebra, highlighting potential connections to the structural theory of finite algebras, including Tame Congruence Theory.