我们为层次化双绑定计算形成了一类交替索引的鲁棒监控合成问题。基本情况是量词前缀 p\, w\, c 的鲁棒逃逸合成问题，当接受通过见证证书表达时，它在级别 ⁰₃ 完整。我们为每个整数 k ≥ 1 定义了一个家族 RESₖ，其中战略参数选择和对抗输入选择交替执行，恰好进行 k 次交替，接受通过一个显式证书见证。我们证明了一个参数完整性定理：如果 k 是奇数，则 RESₖ 是 ⁰₊+₂-完整的；如果 k 是偶数，则 RESₖ 也是 ⁰₊+₂-完整的，所有这些都在可计算的一对多归约下。证明是编码完整的：由于证书包含每个监控评估的显式停机时间界限，因此每个矩阵谓词都是可判定的。该定理得出了一个演算：每增加一次战略环境交替，算术层次级别正好上升一。极性由哪个玩家先行决定。我们通过消除基本接受是由单个存在性证书见证的 ⁰₁ 谓词这一特殊假设，扩展了鲁棒监控合成的基于交替的算术层次分类。首先，我们证明了一个带有确切块合并修正的参数化组合律：如果基本接受谓词位于 ⁰ₐ 中，则存在性战略参数和普遍环境输入之间的 k 次交替会产生一个 ⁰₊+₀+₁（奇 k）或 ⁰₊+₀+₁（偶 k）的合成问题；如果基本接受谓词位于 ⁰ₐ 中，则相应的级别为 ⁰₊+₀（奇 k）或 ⁰₊+₀（偶 k）。第二，我们在一个统一的基本普遍性假设下证明了匹配完整性，该假设捕获了紧下界所需的统一性。第三，我们在允许离散的监控语义下对证书范例进行了压力测试。我们提供了一种新的双侧证书系统（运行证书与反驳证书），具有可判定性验证，并证明基本接受谓词变为 ⁰₂-完整，迫使级别上移并向完整的交替索引层次传播。
Kevin Fathi（周五）研究了这个问题。