Algebraic Characterization of Forest Logics

TL;DR

This paper develops an algebraic framework for forest logics, establishing a correspondence between forest automata pseudovarieties and logical language classes, and proves decidability results for certain logic fragments.

Contribution

It introduces the Moore product for forest automata, creating a lattice isomorphism with forest logic classes, and demonstrates decidability of membership and definability problems.

Findings

Decidability of the FL[EF] fragment definability problem.

Introduction of the Moore product for forest automata.

Conjecture on decidability of the FL[AF] fragment.

Abstract

In this paper we define future-time branching temporal logics evaluated over forests, that is, ordered tuples of ordered, but unranked, finite trees. We associate a rich class FL[$\mathcal{L}$] of temporal logics to each set L of (regular) modalities. Then, we define an algebraic product operation which we call the Moore product, which operates on forest automata, algebraic devices recognizing forest languages. We show a lattice isomorphism between the pseudovarieties of finite forest automata, closed under the Moore product, and the classes of languages of the form FL[$\mathcal{L}$]. We demonstrate the usefulness of the algebraic approach by showing the decidability of the membership problem of a specific pseudovariety of finite forest automata, implying the decidability of the definability problem of the FL[EF] fragment of the logic CTL. Then, using the same approach, we also formulate a conjecture regarding a decidable characterization of the FL[AF] fragment which has currently an unknown decidability status (also in the setting of ranked trees).