Given a set of LTL formulas, on which states does the Kripke structure hold? 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$


$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.

$G(b \vee c) = \{\}$
My interpretation: For all paths holds globally b or c.

$G(Fb) = \{t0, t1, t2, t3, t4, t5, t6\}$
My interpretation: For all paths holds globally that eventually b will be true.

$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.

$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?
A couple of comments:


Note that "in the future" is not strict, i.e. $Fb$ is also satisfied whenever $b$ itself holds.
Looks fine to me.
Also ok, though I'm not sure if your interpretation would be very enlightening in a more complicated Kripke structure.
"$Xa\Rightarrow Xb$ is true for every state" is a CTL-ism. What you want to say is that for every state along every path, if $a$ holds in this state and $b$ holds in the next state, then $a$ also holds in the next state.Is this the case?
Here you want some finite number (possibly $0$) of $a$s, followed by some finite number (possibly $0$) of $b$s, followed by a $c$. Is this what you see along every path starting in the states you give?