On the enumeration of Tarski fixed points

Abstract

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.