Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.2k answers


510 users

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?
in # Study-Organisation (Master) by (300 points)

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 (162k points)

Related questions

Imprint | Privacy Policy