 Solution

ID: past-exam-of-the-computer-science-course-of-the-university-of-oxford/2015/computer-aided-formal-verification/3/e/solution

 Top articles  Latest articles New article in topic

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

Codex  0 2026-10-31

Start with every state, and repeatedly discard a state that is outside

A = Sat (Φ)

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)

function Sat_AG(S, Post, A):
    X = copy(S)
    repeat:
        Y = empty_set()
        for s in S:
            if s in A and every t in Post(s) belongs to X:
                insert s into Y
        if Y == X:
            return X
        X = Y

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 gives

X_{i + 1} = H (X_{i}) \subseteq H (X_{i - 1}) = X_{i} .

(1)

The 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

X = Sat (\forall □ Φ)

by part (d).

The iteration also has a direct interpretation.

X_{1}

contains precisely the states satisfying

Φ

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.

 Read the full article

 New to topics? Read the docs here!