集合自动机与二维数据词逻辑可判定性的极限

我们扩展了数据词上的二变量逻辑，引入形式为 $\widetilde{L}(x,y)$ 的带有护卫的二元谓词，其中若位置 $x$ 和 $y$ 属于同一类且位于 $x$ 和 $y$ 之间的因子属于正则语言 $L$，则该谓词为真。我们描述了单纯 monoid 的类，使得该扩展的二变量逻辑与护卫谓词由 monoid 激活的语言是可判定的，即单纯 monoid，其两侧理想是线性有序的。为此，我们引入一种自动机形式——集合自动机——其等价于 Boja\'nczyk 和 Lasota 的类自动机，从而拥有不可判定的空iness 问题。我们识别了集合自动机的一个子类，称为有序准标准集合自动机，其空iness 问题通过归约到有序多计数器自动机的空iness 问题而可判定。我们表明，扩展了带护卫正则谓词的数据词上的二变量逻辑与 semigroup $S$ 激活的语言在表达上等价于以 semigroup $S$ 的变换集合为 quasi-normal set 自动机。特别地，如果 $S$ 是线性带 monoid，则得到的自动机是有序的，从而可判定性结果随之得出。