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

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.