一句话：证明判定双无限词上给定 MSO 可定义关系是否存在同定义域的 MSO 可定义函数是可判定的。
本文研究双无限词（bi-infinite words）上由 MSO 公式定义的正则关系。核心问题是判定给定关系是否包含一个具有相同定义域的 MSO 可定义函数，即该关系是否可被 MSO 可定义函数一致化。作者证明该判定问题是可判定的。论文指出存在此类一致化的两类障碍：其一是双无限词的非平凡自同构，其二是更微妙的情形——有限离散动力系统中没有任何轨迹可由 MSO 公式选出。该结果刻画了正则关系上 MSO 选择函数的可定义性边界，并推进了无限词自动机与 MSO 逻辑中一致化问题的可判定性研究。
We consider the problem of deciding whether a given mso-definable relation over bi-infinite words contains an mso-definable function with the same domain. We prove that this problem is decidable. There are two obstacles to the existence of such uniformisations: the first is related to the existence of non-trivial automorphisms of bi-infinite words, whereas the second, more subtle obstacle, is related to the existence of finite, discrete dynamical systems, where no trajectory can be selected by an mso formula.
DOI 原文 ·
@inproceedings{paperbot5523,
title = {Uniformisations of Regular Relations Over Bi-Infinite Words},
author = {Grzegorz Fabiański and Michał Skrzypczak and Szymon Toruńczyk},
booktitle = {LICS},
year = {2020},
doi = {10.1145/3373718.3394782}
}