Doubt in LTL model checking exam question 13.02.2019

Question

I am solving exam question 13.02.2019 : Q 7 (b) - 2019.02.13.vrs.solutions.pdf (uni-kl.de)

The automata :

Following is the resultant state transition diagram :

So here only s1 has an infinite run and hence I have to check here for acceptance conditions validity.

I have one doubt here, 

In my understanding, GF (a -> q0) is invalid here because a is always true and q0 is always false.

But then I see a transition to s5 where q0 is true but that path is finite so it will not be considered. 

Is my interpretation correct regarding this ? 

Comments

Direct answer to your question, yes the finite path s1^* s5 is -- as all finite paths -- not considered. We only consider infinite runs in omega-automata.

Answer 1

As far as I can see, the state transition diagram of the automaton is correct, the teaching tool gave me this picture which looks same: 

As we are only interested in infinite runs, we may exclude the finally dead states, and also the unreachable states, of course. What is left is just the self-loop in state s1 that can be taken with any input. That is the only infinite run of this automaton. 

Let's check the acceptance conditions on that path:

1. GF(a->q0) can hold (if we always use input !a)
2. GF(q1->q0) definitely holds since we we never have q1, so q1->q0 does always hold
3. GF(q2->q1) does not hold, since we always have q2 but never q1. 

A path can only be accepted if all conditions would hold, but that is not the case for the only path that exists in the automaton. Hence, the automaton does not accept any word, and therefore the LTL formula is valid.

Comments

I got your point :)
Thanks for this detailed explanation.