Automata for Enriched Trees and Applications

TL;DR

This paper introduces automata models for enriched trees with structured successors, establishing their equivalence to fixed-point logics, and applies these results to characterize monadic second-order logic variants and simplify proofs of existing theorems.

Contribution

It presents new automaton models for enriched trees, proves their equivalence to fixed-point logics, and applies these to characterize logical variants and simplify known theorems.

Findings

Automata models for enriched trees are equivalent to certain fixed-point logics.

Characterizations of monadic second-order logic variants via automata and fixed-point logics.

Simplified proof of the Theorem of Muchnik and its variants for other logics.

Abstract

We study trees where each successor set is equipped with some additional structure. We introduce a family of automaton models for such trees and prove their equivalence to certain fixed-point logics. As a consequence we obtain characterisations of various variants of monadic second-order logic in terms of automata and fixed-point logics. Finally, we use our machinery to give a simplified proof of the Theorem of Muchnik and we derive several variants of this theorem for other logics.