0
$\begingroup$

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$

Given Kripke structure

  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?

$\endgroup$

closed as unclear what you're asking by David Richerby, D.W., Luke Mathieson, Juho, Nicholas Mancuso May 5 '15 at 1:08

Please clarify your specific problem or add additional details to highlight exactly what you need. As it's currently written, it’s hard to tell exactly what you're asking. See the How to Ask page for help clarifying this question. If this question can be reworded to fit the rules in the help center, please edit the question.

  • 3
    $\begingroup$ Your question already includes a complete answer to the original problem but no question about this answer. Thus, only "yes/no" answers may remain, helping neither you nor future visitors. Please read related meta discussions here and here and adjust your question accordingly, e.g. by formulating a specific question about a single element of your answer you are uncertain about. If you just want general feedback, you are welcome to visit us in Computer Science Chat. $\endgroup$ – Raphael Apr 22 '15 at 15:18
  • $\begingroup$ I calculated which state holds for which LTL formula. But I'm not certain if my results are correct, therefore I wanted someone to confirm them. I'll join the chat, if you think my question is more appropriate there. $\endgroup$ – Mad A. Apr 22 '15 at 15:30
1
$\begingroup$

A couple of comments:

  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?
$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – Mad A. Apr 22 '15 at 19:43
  • $\begingroup$ 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$. $\endgroup$ – Klaus Draeger Apr 23 '15 at 11:38

Not the answer you're looking for? Browse other questions tagged or ask your own question.