Past exam of the computer science course of the University of Oxford / 2015 / Computer aided formal verification / 3 / c / Solution

Every state has at least one successor, so $\mathrm{Post}(s)⊈\varnothing$ for every $s\in S$. ThereforeThe 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 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.