# How express this short sentence in CTL?

It's possible that in some following state you have that $$x,y$$ are both true simultaneously.

I have taken a look on Wikipedia: https://en.wikipedia.org/wiki/Computation_tree_logic

and if I understood correctly, the sentence above would look like this in CTL $$EF(x\wedge y)$$

Because $$E$$ alone means "exists (at least one path) where something holds" in this case this something is $$(x\wedge y)$$ and the sentence here is the same as "in some following state" from the sentence above.

$$F$$ means "eventually has to hold" which is the same as in the sentence above "It's possible that".

Can you tell me if it's correct like that pls? It makes sense to me and I feel good about it but I'm very unsure on the way I wrote it combined with this logic $$(x \wedge y)$$. Is it allowed to write it like that?

• We discourage such yes or no questions, since answers are often uninteresting as "yes, that's correct". That being said, your formula looks correct. If you check CTL syntax you will find that it includes ANDs in state formulae. – chi Nov 13 '18 at 23:09
• depending on what "following state" means. If it does not include the current state, then the formula is wrong: You would need to use additional X operator. – Ayrat Nov 17 '18 at 5:18
• In your context, F is related to "following state"---because it talks about time, not about possibilities. "It is possible" is related to E. – Ayrat Nov 17 '18 at 5:20