# Induction February 2019 Exam paper

0 votes
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?

## 1 Answer

0 votes
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 (166k points)

0 votes
1 answer
0 votes
2 answers
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer