= Solution
Every <state> has at least one successor, so $\operatorname{Post}(s)\nsubseteq\varnothing$ for every $s\in S$. Therefore
$$
\boxed{H(\varnothing)=A\cap\varnothing=\varnothing.}
$$
The <empty set> is always a <fixed point>. Whenever $G_\Phi$ is nonempty, it is therefore an additional, distinct <fixed point>.
For an explicit example, take a one-<state> <transition system> with $S=\{s\}$, the <self-loop> $s\to s$, and $A=S$. Then $G_\Phi=S$ and $H$ has the two distinct <fixed points> $\varnothing$ and $\{s\}$. This example meets the requirement of no <terminal states>.
The wording does not guarantee distinct additional <fixed points> for every instance. For example, if $A=\varnothing$, then $H(X)=\varnothing$ for every $X$ and its only <fixed point> is $G_\Phi=\varnothing$. Thus \b[additional fixed points can occur, but need not occur]. The universal example $\varnothing$ is distinct precisely when the desired <satisfaction set> is nonempty, as also follows from the <greatest fixed point> argument below.
Back to article page
