1
$\begingroup$

It's quite a short question: Refering to this Wikipedia article p U q means, that p has to hold at least until at some point q holds.

So, does it mean:

  1. On each path starting from the current state p has to hold in each state until a state is reached in which q holds.
  2. On each path starting from the current state p has to hold in any state before a state is reached in which q holds.

Example: Suppose p holds in s3 and q holds in s5. Let s0 be the starting state and the set of edges given by { (s0,s1),(s1,s2),(s2,s3),(s3,s4),(s4,s5) }. Let's assume p and q don't hold in all the other states. Is p U q satisfied, starting from s0?

$\endgroup$
3
$\begingroup$

$pUq$, as is, is not a well-formulated CTL (or more generally - CTL*) formula. A CTL* formula is a state formula, which starts with has a path quantifier ($A$ or $E$).

$pUq$ is a path formula, which means it refers to a single (linear) computation. A computation satisfies $pUq$ if $p$ holds in every state until $q$ holds (and $q$ must hold at some state).

Translating to CTL, you can talk about two different formulas: $ApUq$ and $EpUq$. The former is true in a state if every path starting from this state satisfies $pUq$. The latter is true in a state if there exists such a path starting from that state.

Does that clear things up?

$\endgroup$
  • $\begingroup$ Yes, it does. Thanks a lot. One further question: If I get the things write, if a state holds p U q then, p must hold in that state. Is that true? $\endgroup$ – 0xbadf00d Feb 1 '14 at 21:40
  • 1
    $\begingroup$ $pUq$ is a path formula, so I guess you mean something like $ApUq$ or $EpUq$. In that case - either $p$ or $q$ must hold in that state. If $q$ holds, then the eventuality is immediately fulfilled. $\endgroup$ – Shaull Feb 2 '14 at 6:43
  • $\begingroup$ So, A[p U q] and E[p U q] are fulfilled when q holds in the current state. Even if p doesn't hold in that state? Seems to make sense. Thanks again. $\endgroup$ – 0xbadf00d Feb 2 '14 at 9:44
  • $\begingroup$ That is correct. $\endgroup$ – Shaull Feb 2 '14 at 9:48

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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