= Solution
Let $G_\Phi=\operatorname{Sat}(\forall\square\Phi)$. By <computation tree logic> semantics, a <state> belongs to $G_\Phi$ exactly when every infinite <path in a transition system> starting there stays in $A=\operatorname{Sat}(\Phi)$ at every position, including position zero. There are no <terminal states>, so every <state> lies at the start of an infinite <path in a transition system>.
If $s\in G_\Phi$, then $s\in A$. For any successor $t$ of $s$, every infinite <path in a transition system> from $t$ can be prefixed with $s$. Hence every such continuation stays in $A$, so $t\in G_\Phi$. Thus $\operatorname{Post}(s)\subseteq G_\Phi$ and $s\in H(G_\Phi)$.
Conversely, if $s\in H(G_\Phi)$, then $s\in A$ and every successor belongs to $G_\Phi$. Every infinite <path in a transition system> from $s$ therefore has its first <state> in $A$ and its entire remaining tail in $A$. Consequently $s\in G_\Phi$. Both inclusions give
$$
\boxed{H(G_\Phi)=G_\Phi,}
$$
so the desired <satisfaction set> is a <fixed point> of $H$.
Back to article page
