0
$\begingroup$

I missed a lot of lectures for this module due to surgery so I'm trying to teach it to myself now. This is the question I've been working on:

enter image description here

First of all, would I be correct in saying that the LTL formulas are b, c and e? CTL are a, d and f?

For (b) I'm guessing the answer is s1 and s3, since those are the only states with b in them.

Looking at (e), this says that the state must always contain b or a, so the answer is s1, s2, s3 and s4 (all states). Is this correct?

(c) is the one I can't get my head round. What exactly is it saying in english?

For now I'll just focus on the LTL stuff, so I just want to get b, e and c 100% correct. Any help is highly appreciated since I'm struggling a bit with this module.

Many thanks in advance!

Improve this question
$\endgroup$

1 Answer 1

Reset to default
0
$\begingroup$

Note that questions of the form "am I correct" are generally not acceptable on this site. Still, your question shows an effort, so here are some answers:

As for your classification to LTL/CTL - you are correct.

Let's look at (b) - it interprets to "always b", which means that in every path starting from the state, b must always hold. This is not the case for any state in the system (since every path eventually reaches s2, in which b does not hold).

As for (e) - it means that in every path, in every suffix, $bUa$ hold, so in every suffix it is true that b holds until a holds. In this system, you are correct that all states satisfy this.

(c) is perhaps easier than the other two - it reads as "next next a", and a state satisfies it if in every path from it, in two steps you will reach "a". In this system, every path gets within two steps to s2, s3, or s4, all of which have "a", so the formula holds.

Improve this answer
$\endgroup$
6
  • $\begingroup$ Hey, apologies - will keep that in mind for the future. Your answers all make perfect sense, thank you. I'm about to start reading up on CTL, but (a) looks pretty straight forward. So it's saying there exists a state who's next state contains 'b'. The only state that holds this property from what I can see is s2, since s3 contains b in it. Is there anything missing from my reasoning? I just want to make sure I have the right idea. Thanks again. $\endgroup$
    – eyes enberg
    Commented Jan 2, 2015 at 19:09
  • $\begingroup$ Are you sure (e) holds for all states? What about from s4 to s2? $\endgroup$
    – eyes enberg
    Commented Jan 2, 2015 at 19:27
  • $\begingroup$ You are right about (a). As for (e): the only way for (e) not to hold is either a path that has $\emptyset$ somewhere before "a", or a path that is $b^\omega$. Neither occurs in this system. $\endgroup$
    – Shaull
    Commented Jan 2, 2015 at 20:59
  • $\begingroup$ But doesn't b U a mean b must happen before a? This isn't always the case in the diagram given $\endgroup$
    – eyes enberg
    Commented Jan 2, 2015 at 23:13
  • 1
    $\begingroup$ Can't thank you enough, your answers have been very helpful. $\endgroup$
    – eyes enberg
    Commented Jan 3, 2015 at 13:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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