Logics with rigidly guarded data tests

TL;DR

This paper introduces a logical framework for recognizing data languages using orbit finite data monoids, connecting algebraic, logical, and automata-theoretic perspectives, and extends these concepts to generic data structures.

Contribution

It defines a new monadic second-order logic with data tests that characterizes data languages recognized by orbit finite data monoids, including aperiodic variants.

Findings

Logic captures exactly the data languages recognized by orbit finite data monoids

First-order fragment corresponds to aperiodic orbit finite data monoids

Variants of the logic recognize data languages via unambiguous finite memory automata

Abstract

The notion of orbit finite data monoid was recently introduced by Bojanczyk as an algebraic object for defining recognizable languages of data words. Following Buchi's approach, we introduce a variant of monadic second-order logic with data equality tests that captures precisely the data languages recognizable by orbit finite data monoids. We also establish, following this time the approach of Schutzenberger, McNaughton and Papert, that the first-order fragment of this logic defines exactly the data languages recognizable by aperiodic orbit finite data monoids. Finally, we consider another variant of the logic that can be interpreted over generic structures with data. The data languages defined in this variant are also recognized by unambiguous finite memory automata.