CTL conversion

Question

Hello,

while learning for the VRS exam, I took a look at some old exams. In the exam from February 2020, Problem 8 a, \phi_4,  we are asked to convert to CTL. There is one step, where the following is done: we have EXXFGE[1 SU (Ab)] which is converted to EXXFGE[1 SU b] and I do not get how this can express the same.

I would be happy if someone could try to explain this to me.

Thanks in advance

Answer 1

By the semantics, Aphi holds in a state if all infinite paths leaving that state satisfy phi. A variable like b is a state formula, and state formulas hold on an infinite path iff they hold on the first state of that path. Hence, Ab holds in a state, if that state does not have outgoing infinite paths at all, or if b holds in that state. 

With this, we could now see that E[1 SU (Ab)] is equivalent to E[1 SU b], and we have the following

    E[1 SU (Ab)]
    = E[1 SU (b | A false)]
    = E( [1 SU b] | [1 SU (A false)])
    = E[1 SU b] | E[1 SU (A false)]
    = E[1 SU b]

In the last step, you have to understand that E[1 SU (A false)] is false: E demands that there must be an infinite path where 1 holds until a state is found on that path where A false holds. However, A false holds in states that have no infinite outgoing paths, and therefore this formula cannot hold on a state on an infinite path.

We can then continue with 

    EXXFGE[1 SU b] 
    = EXXFGEF b
    = EX EX EF EG EF b