2
$\begingroup$

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? : /

Improve this question
$\endgroup$

1 Answer 1

Reset to default
4
$\begingroup$

You can learn a lot about CTL at Wikipedia page.

The sentence you need to write, expressed more closely in the vocabulary of CTL operators, would be
Along all paths starting from current state, it always has to hold that there exists at least one path where $p$ eventually is true.

I think you can take it from there, but comment if you have troubles.

hint: The operators you will need to use are $F$, $A$, $E$ and $G$.

Improve this answer
$\endgroup$
4
  • 1
    $\begingroup$ 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? $\endgroup$
    – tenepolis
    Nov 11, 2018 at 10:07
  • 2
    $\begingroup$ It is correct. If you are sometimes not sure, you can always (edit: maybe not always, depending on strictness of a language) use additional parentheses, giving you A(G(E(Fp))). $\endgroup$
    – Sandro Lovnički
    Nov 11, 2018 at 11:33
  • 1
    $\begingroup$ 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$? $\endgroup$
    – tenepolis
    Nov 11, 2018 at 11:43
  • 1
    $\begingroup$ Your understood it pretty good, but missed the last part - “...is ALWAYS true in future” - which requires a $G$. So we have $AGFEGp$. $\endgroup$
    – Sandro Lovnički
    Nov 11, 2018 at 11:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.