Reducing infinite paths of a transition system to its set of sets of states Consider a transition system defined by $\langle S,T \rangle$, where $S$ is a set of states and $T \subseteq S \times S$ is a set of transitions, where $T$ is total, i.e. for every state $s$ there is at least one outgoing transitions $(s,s') \in T$.
Each path corresponds to a set of states, namely, the states visited along that path.  Given a transition system $\langle S,T \rangle$ and an initial state $s_0 \in S$, I would like an algorithm that outputs the list of all sets of states that can arise from all infinite paths in $\langle S,T \rangle$ that start at $s_0$.
As a trivial example consider $S = \{s_0, s_1, s_2 \}$, $T = \{(s_0,s_1),(s_0,s_2),(s_1,s_1),(s_2,s_2)\}$, with initial state $s_0$; I would like the algorithm to output $\{s_0,s_1\}, \{s_0,s_2\}$.
Is there an algorithm for this problem?
I believe this can be accomplished with strongly connected components, but I don't know what to search for in the literature.
Since the set you want to output can be exponential in the size of the transition system, there is clearly no polynomial algorithm to enumerate it.
Thus, let's focus on an exponential time solution. To this end, it is actually quite easy to find a naive algorithm:
For every subset $Q\subseteq S$ (that contains $s_0$), in order to check whether $Q$ should be outputted by the algorithm, look at the subgraph induced by $Q$, and check whether there is a path from $s_0$ that goes through all the vertices in the induced subgraph.
One way to do the latter, is to indeed decompose the subgraph to its strongly connected components (SCCs), then look at the tree of SCCs, and make sure it's simply a directed path from $s_0$. If it is not a path, then you cannot traverse the entire set $Q$, as you would need to select a branching in the tree from which you cannot go back.
Thus, the test of whether $Q$ should be outputted can be done in polynomial time.