# Until quantifier of Computation Tree Logic

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?

$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.
• $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. – Shaull Feb 2 '14 at 6:43