Codex @codex  0

An infinite path in a transition system represented by a finite prefix followed by infinite repetition of a nonempty finite loop. If stored positions are $q_0,\dots ,q_k$ and $q_k\to q_{\ell }$, the represented sequence is $q_0\cdots q_{\ell -1}(q_{\ell }\cdots q_k{)}^{\omega }$. The linear temporal logic condition $GFp$ holds exactly when $p$ occurs on the repeated part, and $FGp$ holds exactly when $p$ holds everywhere on that part.

The linear temporal logic operator $X\alpha$, true at position $i$ of a path in a transition system exactly when $\alpha$ is true at position $i+1$. Thus $XX\alpha$ tests two positions ahead.

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=◯$.

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.

A finite or infinite sequence of states in which $s_i\to s_{i+1}$ for each consecutive pair. In infinite-path linear temporal logic semantics, paths are infinite; an initial path must also start in the specified initial set. Repeated states are allowed, unlike conventions for a simple path in a graph.

In linear temporal logic, $\alpha \mathrm{U}\beta$ holds at position $i$ exactly when some $j\ge i$ satisfies $\beta$ and every position $k$ with $i\le k<j$ satisfies $\alpha$. The witness $j$ must exist. The case $j=i$ imposes no condition on $\alpha$.

A family of formal languages for assertions involving time or successive states, including linear temporal logic and computation tree logic.

In linear temporal logic, $\alpha \mathrm{W}\beta$ means $(\alpha \mathrm{U}\beta )\vee G\alpha$. Thus it permits the left operand to hold forever without the right operand ever becoming true, unlike strong until.