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:


On each path starting from the current state p has to hold in each state until a state is reached in which q holds.
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.

Does that clear things up?