= Solution
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 define
$$
\boxed{q_{ux}\to q_{yz}\quad\Longleftrightarrow\quad R(u,x,y,z)=y\lor(x\land z)=1.}
$$
The 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\lor 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}$, is
$$
A_R=\begin{pmatrix}
0&0&1&1\\
0&1&1&1\\
0&0&1&1\\
0&1&1&1
\end{pmatrix}.
$$
The <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.
\Image[/past-exam-of-the-computer-science-course-of-the-university-of-oxford/2015/formal-verification-2015-transition-system.png]
{title=Four-state transition system with current bits (u, x), next bits (y, z), and relation y or (x and z)}
Back to article page
