We study the problem of enumerating Tarski fixed points on finite lattices. We derive query complexity lower bounds for finding three or more Tarski fixed points of isotone maps and the subclasses of increasing and decreasing isotone maps. Specifically, we show that any deterministic or bounded-error algorithm must perform asymptotically as many queries in the worst case as the lattice width for isotone maps, which is exponential for the lattice of binary relations and other relevant lattices. We also present two enumeration algorithms for fixed points of increasing or decreasing isotone maps based on depth-first and flashlight search. Both algorithms run in polynomial space on polynomial-height lattices, but are particularly suitable in terms of applicability and runtime performance on different lattices, as they build on differing properties of the underlying lattice. Finally, we discuss the enumeration of Tarski fixed points on the lattices of binary relations, quasiorders and equivalences, demonstrating that the presented algorithms run in polynomial space on these lattices and perform with polynomial delay whenever the problem of finding three or more fixed points is neither NP-hard nor has an exponential query lower bound. We exemplify how these results can be used to list instances of various models of behavioral or role equivalence, specifically deriving a polynomial-space algorithm that enumerates bisimulations with $\mathcal O(n^3m)$ delay on a transition system with $n$ states and $m$ transitions.

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