高阶不动点逻辑模型检测的复杂度

高阶不动点逻辑（HFL）是简单类型 λ-演算与模态 λ-演算的混合体。这使其成为一种高表达力的时序逻辑，能够表达模态 λ-演算无法表达的各种有趣的程序正确性性质。本文为其模型检测问题提供了复杂度结果。特别地，我们考虑了仅使用有界阶 k 和元数 m 的类型所构建的 HFL 片段。我们证明了模型检测每个此类片段的完全复杂度为 k 重指数时间。对于上界，我们使用不动点消除来获得可达性博弈，该博弈的规模相对于公式大小呈单指数增长，相对于底层转换系统的大小呈 k 重指数增长。这些博弈可以在确定性线性时间内求解。作为一个简单的推论，我们得到了每个此类片段的表达复杂度的指数时间上界。下界是通过对具有 (k-1) 重指数空间界限的交替图灵机的字问题进行归约来建立的。由于存在该类型的固定机器，其字问题相对于 k 重指数时间已经是困难的，因此作为一个推论，当 m 大于 3 时，我们得到了 HFL 片段的数据复杂度的 k 重指数时间完全性。这也产生了表达力上的一个层级结果。