# How do you correctly write this sentence as a CTL formula?

Sentence: From every reachable state it is possible to reach a state where $$p$$ is true.

How do you write this sentence as a CTL formula? So far I only dealt with CTL syntax and trees but maybe it will also be asked in a test how you convert a sentence to a CTL formula..

So I've read that $$AX$$ means all next.

Then $$AXp$$ should mean in all next states $$p$$ is true.

Now I only need the first part of the sentence: From every reachable state it is possible to reach

But how would this be expressed and how do you connect it with the $$AXp$$ I got?

I hope you can help me because on the internet I couldn't find some example like that? : /

Along all paths starting from current state, it always has to hold that there exists at least one path where $$p$$ eventually is true.
hint: The operators you will need to use are $$F$$, $$A$$, $$E$$ and $$G$$.
• Thank you very much for help! Then I think the answer is $AGEFp$? If that's correct, I'm still not sure about the syntax. Can I write it like that? – tenepolis Nov 11 '18 at 10:07
• Glad to hear, thanks so much :D Just another example I found, maybe you can check if I did it correct: "In all paths you sometime/eventually reach a state where it's possible that $p$ is always true in future." I think "in all paths" means $AG$, "sometime/eventually reach a state" is $F$, "where it's possible that" is $E$. So in total that should be $AGFEp$? – tenepolis Nov 11 '18 at 11:43
• Your understood it pretty good, but missed the last part - “...is ALWAYS true in future” - which requires a $G$. So we have $AGFEGp$. – Sandro Lovnički Nov 11 '18 at 11:59