[Solved]: Given this transition system, for which states are these (very basic) LTL formulas fulfilled?

Problem Detail: 

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:

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!

Asked By : eyes enberg

Answered By : Shaull

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.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/35865

3.2K people like this

 Download Related Notes/Documents