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

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.

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?

1. Note that "in the future" is not strict, i.e. $Fb$ is also satisfied whenever $b$ itself holds.
4. "$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?
5. 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?
• Hello Klaus, thanks for your input. AD1: So t1 and t3 are states that satisfy $Fc$, is that correct? AD4: I feel like I didn't understand the Ne$X$t operator correctly. Let's only look at $Xa \Rightarrow Xb$, that LTL formula would be satisfied for every state $s0,...,s6$ right? AD5: Yes exactly. There must be at least one state where $c$ is true. Befor that the state must be a set of a's (i.e. aaaaac) a set of b's (bbc) or a set of a's followed by b's followed by at least one c (aaabbbc). Also do you think the states for #4 and #5 are correct disregarding from the interpretation? – Mad A. Apr 22 '15 at 19:43
• Ad 4: You may be thinking of the CTL formula $EXa\Rightarrow EXb$. It is important to remember that LTL semantics is defined in terms of traces; $Xa\Rightarrow Xb$ means that if the second state on a trace satisfies $a$, then it also satisfies $b$. Ad 5: Nothing forces you to ever leave $t4$. – Klaus Draeger Apr 23 '15 at 11:38