We investigate an operator on classes of languages. For each class $C$, it outputs a new class $FO^2(I_C)$ associated with a variant of two-variable first-order logic equipped with a signature$I_C$ built from $C$. For $C = \{\emptyset, A^*\}$, we get the variant $FO^2(<)$ equipped with the linear order. For $C = \{\emptyset, \{\varepsilon\},A^+, A^*\}$, we get the variant $FO^2(<,+1)$, which also includes the successor. If $C$ consists of all Boolean combinations of languages $A^*aA^*$ where $a$ is a letter, we get the variant $FO^2(<,Bet)$, which also includes ``between relations''. We prove a generic algebraic characterization of the classes $FO^2(I_C)$. It smoothly and elegantly generalizes the known ones for all aforementioned cases. Moreover, it implies that if $C$ has decidable separation (plus mild properties), then $FO^2(I_C)$ has a decidable membership problem. We actually work with an equivalent definition of \fodc in terms of unary temporal logic. For each class $C$, we consider a variant $TL(C)$ of unary temporal logic whose future/past modalities depend on $C$ and such that $TL(C) = FO^2(I_C)$. Finally, we also characterize $FL(C)$ and $PL(C)$, the pure-future and pure-past restrictions of $TL(C)$. These characterizations as well imply that if \Cs is a class with decidable separation, then $FL(C)$ and $PL(C)$ have decidable membership.
翻译:我们研究语言类上的一个算子。对于每个类 $C$,该算子输出一个新类 $FO^2(I_C)$,该类别与基于 $C$ 构造的签名 $I_C$ 所装备的二变量一阶逻辑变体相关联。当 $C = \{\emptyset, A^*\}$ 时,我们得到装备线性序的变体 $FO^2(<)$;当 $C = \{\emptyset, \{\varepsilon\},A^+, A^*\}$ 时,我们得到包含后继关系的变体 $FO^2(<,+1)$;若 $C$ 由所有形如 $A^*aA^*$(其中 $a$ 为字母)所构成的语言的布尔组合组成,则我们得到包含"介于关系"的变体 $FO^2(<,Bet)$。我们证明了类 $FO^2(I_C)$ 的通用代数刻画,该刻画平滑而优雅地推广了前述所有已知案例,并且进一步指出:若 $C$ 具有可判定的分离性(加上温和性质),则 $FO^2(I_C)$ 的隶属问题可判定。实际上,我们采用等价于 \fodc 的基于一元时序逻辑的定义来开展工作。对于每个类 $C$,我们考虑一元时序逻辑 $TL(C)$ 的变体,其未来/过去模态依赖于 $C$ 且满足 $TL(C) = FO^2(I_C)$。最后,我们还刻画了 $TL(C)$ 的纯未来与纯过去限制类 $FL(C)$ 和 $PL(C)$,这些刻画同样表明:若 $C$ 是具有可判定分离性的类,则 $FL(C)$ 和 $PL(C)$ 的隶属问题可判定。