Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.3k answers

1.7k comments

557 users

0 votes

Hello,

while learning for the VRS exam, I took a look at some old exams. In the exam from February 2020, Problem 8 a, \phi4,  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

in * TF "Emb. Sys. and Rob." by (440 points)

1 Answer

+1 vote

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 
by (170k points)

Related questions

0 votes
1 answer
asked Aug 31, 2022 in * TF "Emb. Sys. and Rob." by ss (160 points)
0 votes
1 answer
0 votes
1 answer
asked Aug 30, 2022 in * TF "Emb. Sys. and Rob." by ss (160 points)
0 votes
2 answers
Imprint | Privacy Policy
...