How to interpret specific type of CTL/CTL* formula

Question

Q: 13.02.2019 : Q 8 (e) : 2019.02.13.vrs.solutions.pdf (uni-kl.de)

In this question I am having some trouble in figuring out the branching.

Like in S1 E ((Fb) & EG!a) :

-> The outer E says there exist a path on which Fb & EG!a holds. Suppose we have selected a path s0 -> s2, now :

Q Do I need to satisfy ((Fb) & EG!a) on that path only (s0 -> s2)? or it means choose any path from initial state only ?

Q And for the internal E how should I interpret this as a new branch on that path i.e from s2 or it refers to a branch from initial state only ?

Could you please explain how to intuitively think about these types of problems where paths are defined inside bracket as well ?

How to branch from where to branch ?

Answer 1

If you want to show that E ((Fb) & EG!a) holds in state s0, then it is sufficient to prove that one of the infinite outgoing paths in state s0 satisfy (Fb) & EG!a. Selecting the path s0->s2 obviously satisfies F b since on that path b holds when we reach state s2. We also have EG!a at the beginning of the path s0->s2 since in state s0 there is a path namely s0->s1 that satisfies G!a. 

The new path in an inner formula like EG!a can be chosen in a position of the path considered by the outer formula. Since the formula EG!a did not occur behind a temporal operator, it was at position 0, i.e., state s0, but it would be different for E ((Fb) & XEG!a). Here, we would have to find a path starting in s2 (which does not exist).

Comments

How to branch and where to branch is exactly determined by the semantics. If we consider a path for the outer E, and evaluate the path formula on that path where a sub formula Epsi is involved, then the inner formula's semantics determines when we have to use a truth value of the inner formula Epsi. That depends on the formula that we evaluate on the path.