Infinite path in Kripke structures

Question

I saw the lecture and read slides about infinite path, so if I formulate it in a general way then infinite path of Kripke structure K is all the states after removing deadend states and unreachable states. Is it right ? if no could you please explain a bit about how can I compute the infinite path from K ?

Answer 1

No, it is much simpler. After repeatedly removing the deadend states (those states that have no successors), only infinite paths are left. If the Kripke structure is generated from a FSM where all states can react to all inputs, then you just have to remove the deadend states.

Unreachable states are another issue independent of finite paths. As these states are unreachable, they do not matter, and therefore, you can remove them also, regardless whether they have finite or infinite paths.

Comments

Thanks for this clarification.