General question on tasks relating to Kripke structures

Question

I have some short questions regarding Kripke structures:

If a task asks to e.g. "compute reachable states symbolically" is it required to perform a computation or can I just write them down from looking at the structure?

If a task asks for Initial/Reachable states, should generally deadends be included or not? Because I think I have come across tasks where they were included and where they weren't. E.g. if I have an initial state that is a deadend and a root, should I always list it as an initial and reachable state?

Answer 1

If you are asked to compute it symbolically, then please exhibit the computation steps with the transition relation formula. You can in the end manually check whether you'd have found the same states by hand.

I think when converting from Automata to Kripke structure, we removed the freshly introduced deadends. If in doubt, just write that you were not sure whether to remove these states (list them) from the initials as they were deadends.