# Induction February 2019 Exam paper

Problem 11. c) While computing ΨReach, I am not sure, what is the approach that is being used here. What is the transitional relation that is being using to compute existential successors. I don't see that relation anywhere in that question. How do we solve this?

Problem 11c is still part of problem 11 and refers still to the structure defined at the beginning of problem 11. Thus, the transition relation is a∧((b∧c)↔¬b′)∧(c′↔(¬b∧¬c)) and the initial states are b↔c.

The reachable states are those states that are either (1) initial states or (2) reachable with a transition from a reachable state. That can be expressed as a fixpoint which is mu y. (Init ⋁ <:>y) and hence, we perform a fixpoint iteration: Actually, we should start with y0 = \{\}, but that leads then to y1 := Init, so that we started in the solution of 11c directly with Phi_0 := Init. After this, we continue by computing y{i+1} := (Init ⋁ <:>y{i}) which simply means we are adding successor states until we find a fixpoint.
by (162k points)