识别一阶逻辑中带加法与序可定义实数集的 Büchi 自动机

本工作考虑读取固定进制下非负实数编码的弱确定性 Büchi 自动机。实数自动机是指识别一个实数集所有元素编码的自动机。文中解释了如何在线性时间内判定一个给定极小弱确定性 RNA 所识别的实数集是否为 ${FO}[\mathbb R;+,<,1]$-可定义。此外，还解释了如何在拟二次（分别为拟线性）时间内计算一个存在性（分别为存在-全称性）${FO}[\mathbb R;+,<,1]$-公式，该公式定义了自动机所识别的实数集。文中还表明，Muchnik 和 Honkala 为自然数向量自动机给出的技术同样适用于实数向量自动机。这意味着某些问题，例如判定一个实数元组集 $R\subseteq\mathbb R^{d}$ 是否为 $(\mathbb R^{d},+)$ 的子半群或是否为 ${FO}[\mathbb R;+,<,1]$-可定义，是可判定的。