= Solution
Denote the three families found in part (a) by $A=(s_0s_1)^\omega$, $B_n=(s_0s_1)^n s_2^\omega$ and $C_m=s_3^m s_4s_5^\omega$, where $n,m\geq1$. All are fair <paths in a transition system>. The verdicts are
$$
\boxed{(TS\models_{\mathrm{fair}}\varphi_i)_{i=1}^6
=(\text{false},\text{false},\text{false},\text{false},\text{true},\text{false}).}
$$
Each verdict follows from the infinite <path in a transition system> semantics, rather than from a finite prefix alone.
For $\varphi_1=FGa$, take $C_1=s_3s_4s_5^\omega$. From $s_4$ onwards, $a$ is always false, so there is no time after which $a$ is always true. Therefore \b[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 $\varphi_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 \b[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\geq2$, 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 $\varphi_3=Ga$, the fair <path in a transition system> $C_1$ reaches $s_4$, where $a$ is false. Thus \b[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 $\varphi_4=b\mathbin{\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 \b[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 $\varphi_5=b\mathbin{\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 \b[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 $\varphi_6=(XXb)\mathbin{\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 \b[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\geq2$ 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.
Back to article page
