To establish that some set X is a subset of greatest fixpoint nu f, we routinely show that X is a post-fixpoint, ie., X is a subset of f(X). This is a straightforward, constructive way of proving greatest fixpoints. However, for least fixpoints, constructive approaches such as fixpoint iteration break down when we consider subset lattices over infinite sets.

In this talk, we introduce support orderings, along with general lattice-theoretical results, that formalize the dependencies between states that satisfy given fixpoint formulas. This, in essence, gives a purely semantic, constructive account of the least and greatest fixpoints over monotonic functions over subset lattices. We will show how this can be used to reason about least fixpoints in the mu-calculus over infinite-state systems.
This is joint work with Rance Cleaveland.