On the enumeration of Tarski fixed points

TL;DR

This paper investigates the complexity of enumerating Tarski fixed points on finite lattices, establishing lower bounds, proposing algorithms, and analyzing their performance on various lattice structures.

Contribution

It introduces new enumeration algorithms for Tarski fixed points, analyzes their space and runtime complexity, and applies these results to models of behavioral and role equivalence.

Findings

Query complexity lower bounds are exponential for certain lattices.

Two polynomial-space enumeration algorithms are proposed for increasing/decreasing isotone maps.

Algorithms perform with polynomial delay on specific lattices like binary relations, quasiorders, and equivalences.

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.