Question

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

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top