线性序数据域上寄存器自动机的 Church 综合

在 Church 综合博弈中，两名玩家 Adam 和 Eve 在一个有限字母表上交替选取元素，进行无限轮次。若这一无限交互所形成的 omega-字属于给定语言 S（称为规约），则 Eve 获胜。众所周知，对于 omega-正则规约，判定 Eve 是否存在无论 Adam 如何行动都能强制满足规约的策略是可判定的。我们研究将 Church 综合博弈扩展到线性序数据域 (Q, <) 和 (N, <)。在此设定下，Adam 与 Eve 的无限交互产生一个 omega-数据字，即域中元素的无限序列。我们在规约由寄存器自动机给出的情形下研究该问题。此类自动机由有限自动机配备有限个寄存器构成，可在寄存器中存储数据值，并据此与按线性序到达的数据值进行比较。然而，即便对确定性寄存器自动机，(N, <) 上的 Church 博弈也是不可判定的。因此，我们引入单边 Church 博弈，其中 Eve 在有限字母表上行动，而 Adam 仍操纵数据。我们证明它们是确定的，且判定获胜策略的存在性在 ExpTime 内，对 Q 和 N 均成立。这源于对约束序列的研究，其抽象了寄存器自动机的行为，并允许我们将 Church 博弈归约到 omega-正则博弈。我们给出了单边 Church 博弈在转换器综合问题上的一个应用。在该应用中，转换器建模一个反应式系统（Eve），其根据与向系统输入数据的环境（Adam）的交互，输出存储于其寄存器中的数据。