论文标题
捕获双仿真的指数时间复杂性类别
Capturing Bisimulation-Invariant Exponential-Time Complexity Classes
论文作者
论文摘要
Otto的定理表征了三拟合不变的ptime查询在图上的ptime查询，就像可以在多核Mu-calculus中配制的那些，呈现在Immerman-Vardi定理上，该定理表征了ptime（超过有序结构），这是通过最小的固定点具有最小固定点的。该连接已扩展以表征双仿真的exptime通过在谓词上的函数的函数扩展，从而利用Immerman通过二阶逻辑以最小的固定点来表征Immerman对Exptime的表征。在本文中，我们表明，在指数时间层次结构中，所有类别的三拟合不变版本具有逻辑对应物，这些版本是通过高阶函数作为多层MU-Calculus的扩展而产生的。这是由于Freire和Martins的最小固定点的高阶逻辑（k+1）的k-extime表征。
Otto's Theorem characterises the bisimulation-invariant PTIME queries over graphs as exactly those that can be formulated in the polyadic mu-calculus, hinging on the Immerman-Vardi Theorem which characterises PTIME (over ordered structures) by First-Order Logic with least fixpoints. This connection has been extended to characterise bisimulation-invariant EXPTIME by an extension of the polyadic mu-calculus with functions on predicates, making use of Immerman's characterisation of EXPTIME by Second-Order Logic with least fixpoints. In this paper we show that the bisimulation-invariant versions of all classes in the exponential time hierarchy have logical counterparts which arise as extensions of the polyadic mu-calculus by higher-order functions. This makes use of the characterisation of k-EXPTIME by Higher-Order Logic (of order k+1) with least fixpoints, due to Freire and Martins.
