An Application of the Feferman-Vaught Theorem to Automata and Logics for<br> Words over an Infinite Alphabet

TL;DR

This paper applies a specialized Feferman-Vaught theorem to develop automata and logical frameworks for finite words over infinite alphabets, ensuring closure, decidability, and expressive power.

Contribution

It introduces a novel automata model and logical characterizations for infinite alphabet words based on the Feferman-Vaught theorem, extending to more expressive relations.

Findings

Automata for infinite alphabet words have good closure and decidability properties.

Extended formalism allows expressing relations like equality with maintained decidability.

New decidable logical frameworks for words over infinite alphabets.

Abstract

We show that a special case of the Feferman-Vaught composition theorem gives rise to a natural notion of automata for finite words over an infinite alphabet, with good closure and decidability properties, as well as several logical characterizations. We also consider a slight extension of the Feferman-Vaught formalism which allows to express more relations between component values (such as equality), and prove related decidability results. From this result we get new classes of decidable logics for words over an infinite alphabet.