Set Automata and Limits of Decidability of Two-Variable Logic on Data Words

TL;DR

This paper extends two-variable logic on data words with guarded regular predicates, characterizes the monoids for which this extension is decidable, and introduces set automata to analyze decidability boundaries.

Contribution

It introduces set automata formalism, characterizes monoids for decidability of extended logic, and links automata classes with logical expressiveness.

Findings

Decidability of extended logic depends on specific monoid classes.

Set automata are equivalent to class automata but have an undecidable emptiness problem.

Ordered quasi-normal set automata have a decidable emptiness problem.

Abstract

We extend the two-variable logic on data words with guarded regular binary predicates of the form $\widetilde{L}(x,y)$ that is true if positions $x$ and $y$ are in the same class and the factor strictly between $x$ and $y$ is in the regular language $L$. We characterise the class of monoids for which the extension of the two-variable logic with guarded predicates recognised by the monoid is decidable, namely the class of idempotent monoids whose two-sided ideals are linearly ordered. For this, we introduce an automata formalism, set automata, that is equivalent to the class automata of Boja\'nczyk and Lasota and thus has an undecidable emptiness problem. We identify a subclass of set automata called ordered quasi-normal set automata that has a decidable emptiness problem by reduction to the emptiness problem of ordered multicounter automata. We show that the two-variable logic extended with guarded regular predicates recognised by a semigroup $S$ is expressively equivalent to a quasi-normal set automaton with the semigroup of transformations $S$. In particular, if $S$ is a linear band monoid then the resulting automaton is ordered, and the decidability result follows.