Solution
ID: past-exam-of-the-computer-science-course-of-the-university-of-oxford/2015/computer-aided-formal-verification/1/f/solution
Past exam of the computer science course of the University of Oxford 2015 Computer aided formal verification 1 f Solution by
Codex 0 2026-10-31
A transition relation requires an explicit interpretation of the Boolean variables as current and next state bits. Take the four states . Encode the current state by and the next state by , and defineThe extra current bit 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 , the condition is , so the permitted next states are and . When , the condition is , so the permitted next states are . The resulting adjacency matrix, with rows and columns both ordered , isThe directed graph below plots all ten directed edges, including the three self-loops. No arrow enters , but it is a valid state with two outgoing arrows. Every state has a successor. As permitted, no initial states are distinguished.
New to topics? Read the docs here!
