= Solution
Start with every <state>, and repeatedly discard a <state> that is outside $A=\operatorname{Sat}(\Phi)$ or has any successor outside the current candidate <set>. Use a fresh <set> on each iteration so that the displayed procedure computes exactly $H(X)$:
``
function Sat_AG(S, Post, A):
X = copy(S)
repeat:
Y = empty_set()
for s in S:
if s in A and every t in Post(s) belongs to X:
insert s into Y
if Y == X:
return X
X = Y
``
This is <fixed-point iteration> $X_0=S$, $X_{i+1}=H(X_i)$. The first step gives $X_1=A$, because every successor is a <state> of $S$. Thus $X_1\subseteq X_0$. If $X_i\subseteq X_{i-1}$, the <order-preserving function> property gives
$$
X_{i+1}=H(X_i)\subseteq H(X_{i-1})=X_i.
$$
The candidate <sets> therefore form a descending chain under <set inclusion>.
Every <fixed point> $Z$ is contained in every $X_i$: initially $Z\subseteq S$, and $Z\subseteq X_i$ implies $Z=H(Z)\subseteq H(X_i)=X_{i+1}$. At return, $X=H(X)$, and $X$ contains every <fixed point>. The returned <set> is consequently the <greatest fixed point>, so $\boxed{X=\operatorname{Sat}(\forall\square\Phi)}$ by part (d).
The iteration also has a direct interpretation. $X_1$ contains precisely the <states> satisfying $\Phi$ now; $X_2$ retains those satisfying it now and at all immediate successors; later rounds extend the checked horizon one step at a time. The stable <set> enforces the condition at every future position.
Back to article page
