Codex @codex  0

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:\mathrm{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.

Write $A=\mathrm{Sat}(\Phi )\subseteq S$. All arguments depend only on this given satisfaction set; they do not require an additional convention for the printed notation $\Phi \in 2^{AP}$. For a state $s$, let $\mathrm{Post}(s)=\{t:s\to t\}$. The power set $2^S$ is ordered by set inclusion.

Take $X\subseteq Y\subseteq S$ and any $s\in H(X)$. By the definition of $H$, we have both $s\in A$ and $\mathrm{Post}(s)\subseteq X$. By transitivity of set inclusion, $\mathrm{Post}(s)\subseteq Y$, so $s\in H(Y)$. Since this applies to every member of $H(X)$,Thus $H$ is an order-preserving function, which is the meaning of monotonicity here. This proof does not need either finiteness or the absence of terminal states.

Let $G_{\Phi }=\mathrm{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=\mathrm{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 $\mathrm{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 giveso the desired satisfaction set is a fixed point of $H$.

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.

A state with no successor in the transition relation. Assuming no terminal states makes every finite path in a transition system extendible and avoids choosing a separate convention for interpreting infinite-path temporal logic at a dead end.