Can deadends in Kripke structures be initial states?

Question

For exercise 3b), we have to submit the initial states of the Kripke structure. The solution is only accepted, if you don't include the initial states, that are deadend states.

But e.g. on slide 13 you can see, that deadend states can be initial states as well. Looking at the definition, I don't see why they shouldn't count as initial states.

I think e.g. the state (!p & !q & !a) should be an initial state in this particular exercise.

Answer 1

I agree with you that formally speaking, initial states may have no outgoing transitions. We can consider such kind of structures, and there is no good argument why that should be forbidden. The semantics of formulas is defined in a way that copes well with deadend states: All universally quantified formulas Aphi would hold in those states while all existentially quantified formulas Ephi would not hold there. Even A false would hold there, and even E true would not hold there.

In practice, such structures are however questionable and should not occur. In particular, reactive systems must have ongoing computations, and if an initial state would not have any infinite path, then this would mean that the system is somehow broken in an initial state. For this reason, you may also have good reasons to define that initial states must have outgoing transitions, but we did not demand this.

So, the exercise tool should be fixed accordingly.