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ńczyk 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.

翻译：我们扩展了数据字上的双变量逻辑，引入了形如$\widetilde{L}(x,y)$ 的受保护正则二元谓词，该谓词在位置$x$和$y$属于同一类别且两者之间的严格子串属于正则语言$L$时成立。本文刻画了使得该扩展逻辑（其受保护谓词可由幺半群识别）可判定的幺半群类，即双边理想呈线性序的幂等幺半群。为此，我们提出了一种与Bojańczyk和Lasota的类自动机等价的自动机形式——集合自动机，其空性判定问题不可判定。我们进一步识别出集合自动机的一个子类——有序准正规集合自动机，通过将其归约为有序多计数器自动机的空性判定问题，证明了该类自动机空性判定的可判定性。我们证明，由半群$S$识别的受保护正则谓词扩展的双变量逻辑在表达性上等价于以$S$为变换半群的准正规集合自动机。特别地，当$S$是线性带幺半群时，所得自动机是有序的，从而可判定性结论成立。