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.