Compute deadends and reachable states symbolically

Question

Hi,

I saw couple of questions from previous year questions papers and final exercise sheet, where it is asked to compute reachable states/dead ends symbolically. However, when I went through exercise sheet and slides, I could find the ways to find predecessor/successors only through symbolically not the deadends/reachable states. I am not sure if I have missed them somehow. Could you please let me know the steps to obtain the same?

Answer 1

The formula []false holds exactly on those states that do not have outgoing transitions. Hence, you can compute these states of a structure by computing the universal predecessors of false.

The reachable states are those that are (1) initial states or (2) reachable from a reachable state. That gives rise to the definition in µ-calculus mu y. (Init | <:>y) which means that you can compute the reachable states by a fix point iteration as given by the above formula, i.e., start with the initial states, then always add existential successor states of the states that you already have.

Comments

Thanks Professor for the quick reply. It is clear now (y)