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

870 questions

988 answers


439 users

0 votes

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 ?

in * TF "Emb. Sys. and Rob." by (2.9k points)

1 Answer

+1 vote
Best answer
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.
by (139k points)
selected by
Thanks for this clarification.

Related questions

Imprint | Privacy Policy