World's most popular travel blog for travel bloggers.

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

, ,
Problem Detail:

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?

#### Answered By : Klaus Draeger

1. Note that "in the future" is not strict, i.e. \$Fb\$ is also satisfied whenever \$b\$ itself holds.
2. Looks fine to me.
3. Also ok, though I'm not sure if your interpretation would be very enlightening in a more complicated Kripke structure.
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?