Given a set of LTL formulas, on which states does the Kripke structure hold? [closed]

Question

I'm currently learning about LTL and CTL formulas and to get a better understanding I try to manually interpret the formulas over a given Kripke structure. Since I'm not 100% sure if my results are correct I would appreciate if anyone can verify them.

Task:

I showed on which states the given LTL formular hold.

Some LTL notation notes:

$X$ equals $\bigcirc$

$G$ equals $\Box$

$F$ equals $\diamond$

1. $Fc = \{\}$

   My interpretation: $Fc$ means that on all paths $c$ holds sometimes the future. Since all paths come along $t4$ it doesn't hold for any state.

2. $G(b \vee c) = \{\}$

   My interpretation: For all paths holds globally b or c.

3. $G(Fb) = \{t0, t1, t2, t3, t4, t5, t6\}$

   My interpretation: For all paths holds globally that eventually b will be true.

4. $G(b \Rightarrow (Xa \Rightarrow Xb)) = \{t0, t1, t2, t3, t4, t5, t6\}$

   My interpretation: Since $Xa \Rightarrow Xb$ is true for every state the implication $b \Rightarrow (Xa \Rightarrow Xb)$ must hold for all states too sinde $? \Rightarrow true$ is always true.

5. $a U (b U c) = \{t1, t3, t4, t5\}$

   My interpretation: Following paths are valid: aaaaabbbc, bbbbc, c, ccc. Therefore the states $t1, t3, t4, t5$ are valid.

So can anybody confirm my results?