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

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.

Let $X$ be any fixed point of $H$. Thenso $X\subseteq A$ and every successor of every member of $X$ belongs to $X$. Take $s_0\in X$ and an arbitrary infinite path in a transition system $s_0{s}_1{s}_2\cdots$ from $s_0$. By mathematical induction, every $s_i$ belongs to $X$: the base case is the choice of $s_0$, and $s_i\in X$ implies $s_{i+1}\in \mathrm{Post}(s_i)\subseteq X$.

Since $X\subseteq A$, the whole path in a transition system stays in $A$. The path in a transition system was arbitrary, so $s_0\models \forall \square \Phi$. Thus $s_0\in G_{\Phi }$, and since $s_0$ was arbitrary in $X$,Part (b) proves that $G_{\Phi }$ itself is a fixed point. Thereforethe greatest fixed point with respect to set inclusion. In fact the same induction works for every $X\subseteq H(X)$, showing why a successor-closed set of good states certifies this universal property.

Start with every state, and repeatedly discard a state that is outside $A=\mathrm{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)$: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 givesThe 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=\mathrm{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.

Yes: the procedure always terminates after finitely many steps. If an iteration does not return, then $X_{i+1}⊊X_i$. Thus at least one state is permanently removed. A finite set of $|S|$ states can suffer at most $|S|$ such strict decreases, after which the next equality test must return. Therefore the procedure makes at mostwhen started from $X_0=S$, counting the final evaluation that detects equality. The bound also covers $S=\varnothing$, where the first evaluation already returns. Each evaluation inspects finitely many states and successors, so every individual step terminates as well. Finiteness, rather than monotonicity alone, supplies this finite termination bound.