= Greatest fixed point
{title2=$\nu X.\,H(X)$}
A <fixed point> of a <function> on a <partially ordered set> that is greater than or equal to every other <fixed point>. For the <order-preserving function> $H(X)=A\cap\{s:\operatorname{Post}(s)\subseteq X\}$ on the <power set> of a finite <transition system> with no <terminal states>, its <greatest fixed point> is the <set> of <states> from which every infinite <path in a transition system> remains in $A$. Iteration from the whole <state space> decreases to this <set>; every strict decrease removes at least one <state>.
Back to article page
