Past exam of the computer science course of the University of Oxford / 2015 / Computer aided formal verification (A12072W1)

Solutions to the paper whose cover dates the examination to 6 June 2015, 2:30–4:00 pm. Source: released examination archive, member 2015-cafv.pdf. All three questions are covered, although candidates were asked to attempt at most two. In the binary decision diagrams, dashed arrows mean zero and solid arrows mean one. In the linear temporal logic calculations, $F=◊$, $G=\square$ and $X=◯$.

Follow the binary decision diagram from its top decision node to a terminal node, choosing the outgoing arrow specified by each tested Boolean variable. If $x=0$, the left $y$ decision node returns $y$, independently of $z$. If $x=1$, the right $y$ decision node returns one when $y=1$ and otherwise returns $z$. Thus the truth table, with rows in the order $(x,y,z)$, is:

Thus the output column of the truth table, in the displayed order, is $\boxed{(0,0,1,1,0,1,1,1)}$. In particular, the skipped $z$ test on the left does not constrain $z$: both values give the same result.

Splitting the Boolean function according to the first tested Boolean variable givesThe identity $y\vee (\neg y\wedge z)=y\vee z$ follows by considering $y=0$ and $y=1$. Using it and distributing Boolean conjunction over Boolean disjunction,The first two terms combine to $y$ because $x\vee \neg x=1$. This also explains the truth table: $y=1$ always makes the output one, while with $y=0$ the output is one exactly when both $x$ and $z$ are one.

For a complete binary decision tree with variable ordering of a binary decision diagram $z<y<x$, first test $z$, then $y$, then $x$ on every branch. The four Boolean cofactors after the first two tests are

The eight terminal nodes, read from left to right in the figure, are $\boxed{0,0,1,1,0,1,1,1}$. The repeated tests are intentional: this is the full binary decision tree before any reduction.

For example, the branch $z=1,y=0,x=1$ ends at one, whereas $z=0,y=0,x=1$ ends at zero. This checks the dependence on $z$ that must survive the later reduction.

A reduced ordered binary decision diagram is obtained by sharing equal terminal nodes, removing a decision node whose two children are equal, and sharing decision nodes with the same tested Boolean variable and the same ordered pair of children. Apply these rules to the binary decision tree in part (c) as follows.

The left panel below is therefore the resulting reduced ordered binary decision diagram. Its full description is

There are $\boxed{4+2=6}$ vertices: four decision nodes and two terminal nodes.

The original binary decision diagram also has four decision nodes and two terminal nodes, and is already reduced for $x<y<z$: the two $y$ decision nodes have different children and no decision node has two equal children. Thus reversing the order has not made this example smaller. Indeed $y\vee (x\wedge z)$ is unchanged by interchanging $x$ and $z$, and the new binary decision diagram is the original one with those two labels exchanged. The uniqueness of a reduced ordered binary decision diagram applies to a fixed variable ordering of a binary decision diagram; it does not assert that every ordering has the same size.

Choose the variable ordering of a binary decision diagram $y<x<z$. The Boolean cofactor with $y=1$ is the constant one, while the Boolean cofactor with $y=0$ is $x\wedge z$. Consequently the right panel in part (d) has the following arrows:Here an entry such as $0\to x$ denotes the zero arrow to the $x$ decision node. There are $\boxed{3+2=5}$ vertices: three decision nodes and two terminal nodes, saving one decision node relative to either of the previous orderings. Testing $y$ first is effective because its one branch settles the entire Boolean function immediately. The ordering $y<z<x$ works equally well.

This is also minimal among ordinary binary decision diagrams for this Boolean function. Each Boolean variable is essential: setting $y=0,z=1$ leaves $f=x$; setting $y=0,x=1$ leaves $f=z$; and setting $x=z=0$ leaves $f=y$. If a Boolean variable were never tested, the represented Boolean function could not depend on it. Thus at least three decision nodes are necessary, and the construction attains that bound.

A transition relation requires an explicit interpretation of the Boolean variables as current and next state bits. Take the four states $q_{00},q_{01},q_{10},q_{11}$. Encode the current state by $(u,x)$ and the next state by $(y,z)$, and defineThe extra current bit $u$ is deliberately unused by the Boolean formula. A four-state transition system normally needs four bits to describe a pair of states; a Boolean formula using only three of them simply describes a transition relation independent of the fourth bit.

When $x=0$, the condition is $y=1$, so the permitted next states are $q_{10}$ and $q_{11}$. When $x=1$, the condition is $y\vee z$, so the permitted next states are $q_{01},q_{10},q_{11}$. The resulting adjacency matrix, with rows and columns both ordered $q_{00},q_{01},q_{10},q_{11}$, isThe directed graph below plots all ten directed edges, including the three self-loops. No arrow enters $q_{00}$, but it is a valid state with two outgoing arrows. Every state has a successor. As permitted, no initial states are distinguished.

Use the two incoming initial arrows in the source figure: $I=\{s_0,s_3\}$. An atomic proposition is true precisely at the states whose displayed labels contain it. In particular, $c$ is false at every state. Hence $GF\neg c$ is true on every infinite path in a transition system, and the first implication in the fairness assumption imposes no restriction.

Write $p=a\wedge b$. The remaining implication is $FGp\to GF\neg b$. By the linear temporal logic duality $\neg FGp=GF\neg p$, it is equivalent tosince $\neg b$ implies $\neg p$. Thus a path is fair exactly when it visits states not labelled with both $a$ and $b$ infinitely often. This condition also follows directly: if $p$ eventually holds forever, then $b$ eventually holds forever and the required $GF\neg b$ is impossible; if $p$ does not eventually hold forever, the implication has a false antecedent.

Every initial path in a transition system in the upper component either alternates forever between $s_0$ and $s_1$, or makes finitely many alternations and then stays at $s_2$. These are all fair: the first visits $s_1$ infinitely often, and the second visits $s_2$ infinitely often; neither state satisfies $a\wedge b$.

In the lower component, a path in a transition system can stay at $s_3$ forever, or leave it after finitely many visits and pass through $s_4$ to $s_5$. The constant path in a transition system $s_3^{\omega }$ is unfair because $a\wedge b$ holds forever while $\neg b$ never holds. Every departing path in a transition system is fair because $s_5$ satisfies neither $a$ nor $b$. Here $v^{\omega }$ means infinite repetition of the finite word $v$. ThereforeThis notation lists initial paths in a transition system. If one instead allows arbitrary starting states, their suffixes starting at $s_1,s_2,s_4,s_5$ are fair as well; the fair paths in a transition system from each initial state, and hence all verdicts below, are unchanged.

Denote the three families found in part (a) by $A=(s_0{s}_1{)}^{\omega }$, $B_n=(s_0{s}_1{)}^n{s}_2^{\omega }$ and $C_m=s_3^m{s}_4{s}_5^{\omega }$, where $n,m\ge 1$. All are fair paths in a transition system. The verdicts areEach verdict follows from the infinite path in a transition system semantics, rather than from a finite prefix alone.

For ${\phi }_1=FGa$, take $C_1=s_3{s}_4{s}_5^{\omega }$. From $s_4$ onwards, $a$ is always false, so there is no time after which $a$ is always true. Therefore the first specification fails, with fair counterexample $C_1$. The path in a transition system $A$ is another fair counterexample, because it encounters $s_1$, where $a$ is false, infinitely often. Each $B_n$ does satisfy $FGa$, since $s_2$ satisfies $a$ forever.

For ${\phi }_2=(X\neg a)\to FGa$, take $A$. Its next state is $s_1$, so $X\neg a$ is true, but $FGa$ is false as just shown. Thus the second specification fails, with fair counterexample $A$. Alternatively, $C_1$ has next state $s_4$, making its antecedent true and its consequent false. For $C_m$ with $m\ge 2$, the next state is still $s_3$, so this implication is true there because its antecedent is false; this does not rescue a universally quantified specification.

For ${\phi }_3=Ga$, the fair path in a transition system $C_1$ reaches $s_4$, where $a$ is false. Thus the third specification fails, with fair counterexample $C_1$. In fact every fair initial path in a transition system reaches $s_1$ or $s_4$, so none satisfies $Ga$.

For ${\phi }_4=b\mathrm{U}G\neg b$, strong until requires an eventual position satisfying $G\neg b$, together with $b$ at every earlier position. On $A$, $b$ is true forever, so $G\neg b$ never holds. Thus the fourth specification fails, with fair counterexample $A$. On each $B_n$, $b$ holds until entry into $s_2$, after which $\neg b$ holds forever. On each $C_m$, $b$ holds until entry into $s_5$, after which $\neg b$ holds forever. These latter paths in a transition system satisfy the strong until requirement.

For ${\phi }_5=b\mathrm{W}G\neg b$, weak until permits either the preceding strong until behavior or $Gb$. Every $B_n$ and $C_m$ satisfies the strong until behavior, and $A$ satisfies $Gb$. These exhaust the fair initial paths in a transition system. Therefore the fifth specification holds on every fair initial path. Allowing the left operand to continue forever is exactly what distinguishes this answer from the previous one.

For ${\phi }_6=(XXb)\mathrm{U}G\neg b$, the two next-time operators belong to the left operand of strong until. The fair path in a transition system $C_1$ has $b$ true at positions zero and one, then false at every position from two onwards. Therefore $G\neg b$ first holds at position two. But $XXb$ is false already at position zero, since $b$ is false at position two. A witness for strong until cannot occur at zero or one, where its right operand is false, or at two or later, where its left operand has already failed. Thus the sixth specification fails, with fair counterexample $C_1$.

Indeed, every fair initial path in a transition system fails the sixth specification. On $A$, the right operand never holds. On $B_n$ and $C_m$, let $j\ge 2$ be the first position of the permanent $\neg b$ tail. The left operand $XXb$ is false at $j-2$, strictly before any possible right-operand witness. This also checks that the two next-time operators cannot be ignored or shifted onto the whole strong until formula.

To apply bounded model checking, seek an initial path in a transition system satisfyingA satisfying assignment for its bounded encoding is enough to disprove the specification. Use a lasso path: positions $q_0,\dots ,q_k$ follow the transition relation, and a final arrow returns from $q_k$ to some $q_{\ell }$, $0\le \ell \le k$. The repeated part is $q_{\ell }\cdots q_k$. On such a lasso path, $GFr$ is equivalent to having $r$ true at some position of the repeated part.

For this example an explicit Boolean formula for the bounded search isHere $I(q)$ means $q\in \{s_0,s_3\}$ and $T(q,r)$ means that the source diagram has the arrow $q\to r$; each can be encoded by finite Boolean variables for the states. The loop requirements are the fairness assumption and the negated specification respectively. Unrolling the transition relation and adding a loop closure is the usual bounded model checking construction.^[ref]

At bound $k=0$, an initial self-loop would be needed. The only such choice is $q_0=s_3$, whose repeated label satisfies $a\wedge b$ and $a$. It violates both loop requirements. The other initial state, $s_0$, has no self-loop. Thus $E_0$ has no satisfying assignment.

At bound $k=1$, chooseBoth required arrows $s_0\to s_1$ and $s_1\to s_0$ exist. At $q_1$, $a$ is false and hence $a\wedge b$ is false, so both repeated-part requirements are true. Equivalently, the label values are $a(q_0)=b(q_0)=b(q_1)=1$ and $a(q_1)=c(q_0)=c(q_1)=0$. These values give a satisfying assignment of $E_1$, representing the fair counterexample $(s_0{s}_1{)}^{\omega }$. ConsequentlyHere the bound counts forward arrows before the returning arrow, so $k=1$ stores two positions and describes a two-state repeated part. There is no need for a completeness bound: the exhibited fair counterexample settles the negative answer. These satisfying assignments are checked directly; no claim of executing an external SAT solver is needed.

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.