关于 Tarski 不动点的枚举

我们研究有限格上 Tarski 不动点的枚举问题。我们导出了寻找保序映射及其递增与递减保序映射子类上三个或更多 Tarski 不动点的查询复杂度下界。具体而言,我们表明任何确定性或有界错误算法在最坏情况下必须执行与格宽度渐近等多的查询次数(对于二元关系格及其他相关格而言是指数级的)。我们还提出了两种基于深度优先和手电筒搜索的、用于递增或递减保序映射不动点枚举的算法。两种算法在多项式高度格上以多项式空间运行,但由于建立在底层格的不同性质之上,它们在适用性和运行时间性能方面于不同格上尤为适用。最后,我们讨论了二元关系、拟序和等价格上 Tarski 不动点的枚举,证明所提算法在这些格上以多项式空间运行,并且当寻找三个或更多不动点的问题既非 NP 难也不具有指数查询下界时以多项式延迟执行。我们举例说明了如何利用这些结果列出各种行为或角色等价模型的实例,具体推导出一个在具有 $n$ 个状态和 $m$ 条转移的转移系统上以 $\mathcal O(n^3m)$ 延迟枚举互模拟的多项式空间算法。