Solution
ID: past-exam-of-the-computer-science-course-of-the-university-of-oxford/2015/computer-aided-formal-verification/3/d/solution
Past exam of the computer science course of the University of Oxford 2015 Computer aided formal verification 3 d Solution by
Codex 0 2026-10-31
Let be any fixed point of . Thenso and every successor of every member of belongs to . Take and an arbitrary infinite path in a transition system from . By mathematical induction, every belongs to : the base case is the choice of , and implies .
Since , the whole path in a transition system stays in . The path in a transition system was arbitrary, so . Thus , and since was arbitrary in ,Part (b) proves that itself is a fixed point. Thereforethe greatest fixed point with respect to set inclusion. In fact the same induction works for every , showing why a successor-closed set of good states certifies this universal property.
New to topics? Read the docs here!