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

915 questions

1k answers

1.4k comments

441 users

0 votes
slide 41 - chapter 7 - temporal logic

I have seen this part of lecture (2-3 times) where this slide has been explained but I am still confused. On left hand side we have CTL form and on right hand side we have non-CTL form?
in * TF "Vis. and Sci. Comp." by (870 points)

1 Answer

0 votes

Just to make sure that we talk about the same slide: 

Now, the answer to your question: If you assume that phi and psi would be CTL formulas, then all the left hand sides would also be CTL formulas and there would not be a problem. However, the slide discusses the problem that in front of a temporal operator we might miss a path quantifier. So, assume you have EF Gp which is not a CTL formula. Then, this slide tells you that you can add for any formula EFphi a path quantifier to obtain EFE phi and that make then EFGp a CTL formula EFEGp. The slide does not say whether the left or right hand side is a CTL formula, but it does say where you can add path quantifiers that you may miss to transform a formula which is not in CTL syntax (but equivalent to a CTL formula) to the CTL syntax.

by (142k points)
Ok. Now I understand. The example you provided is really helpful. Thank you so much.

Related questions

0 votes
1 answer
asked Aug 14, 2020 in * TF "Vis. and Sci. Comp." by Anshu (870 points)
0 votes
1 answer
asked Aug 13, 2020 in * TF "Vis. and Sci. Comp." by Anshu (870 points)
0 votes
1 answer
asked Aug 13, 2020 in * TF "Vis. and Sci. Comp." by Anshu (870 points)
0 votes
1 answer
asked Aug 13, 2020 in * TF "Vis. and Sci. Comp." by Anshu (870 points)
0 votes
1 answer
asked Aug 12, 2020 in * TF "Vis. and Sci. Comp." by Anshu (870 points)
Imprint | Privacy Policy
...