# Some slight confusion with the UNTIL operator in CTL (e.g. a U b)

I've sketched a very small transition system in paint that I'll use as an example.

I want to see if $A(aUb)$ holds for this transition system. From my understanding, this CTL formula is asking if ALL paths satisfy $aUb$. The only path we can take in this example is S0S1S0S1S0S1S0S1...

This path produces the output (1) $aaaaaaaaaaaaaaaaa...$ or (2) $aaaaaaaaaaaaaaab...$

(2) definitely holds - however it's (1) that I'm unsure about. Am I correct in saying that $aUb$ doesn't hold for (1)? Since we can continue looping over a infinitely without eventually reaching b (and because (1) doesn't satisfy the formula, $A(aUb)$ doesn't hold for this transition system).

Have I understood this correctly? I guess the main confusion for me is that there is 1 path but more than 1 possible output.

Any help is much appreciated.

edit: This is the transition system I'm referring to in the comments below

• OK so I guess it would make more sense if S0 had an arrow pointing to another state (S2) which contains {b}. I want to know if FOR ALL paths from S0, a U b is true (so does V (a U b) hold for S0?). I know it holds for S0S2, but S1 has "a" aswell as "b" so if we keep choosing "a", "b" will never be reached, and thus the formula doesn't hold. Is this correct? – eyes enberg Jan 6 '15 at 16:22

You have some misconception regarding transition systems: The alphabet of the system is $2^P$ for some set $P$, and paths induce words over $2^P$. In the first system, there is a single path: $(S_0,S_1)^\omega$, and it induces a single word: $(\{a\},\{a,b\})^\omega$.

Now, this word satisfies $aUb$, since $a$ holds until the secod letter, in which $b$ holds.

The $\forall$ quantifier here is somewhat useless, since there is a single path.

The second system is problematic, since there is nowhere to go to from $S_2$...

• Thank you, this was exactly the answer I needed. This module is finally starting to click – eyes enberg Jan 6 '15 at 19:57

A small addendum to @Shaull's anwswer, which is completely correct: for the output (1), $aaaaaaaaa\ldots$, you suggested (if it were possible in your transition system), your assumption that the formula does not hold is correct. The formula $A [a U b]$ does not hold on such a path; Wikipedia gives the following definition:

$\bigg( (\mathcal{M}, s) \models A[\phi_1 U \phi_2] \bigg) \Leftrightarrow \bigg( \forall \langle s_1 \rightarrow s_2 \rightarrow \ldots \rangle (s=s_1) \exists i \Big( \big( (\mathcal{M}, s_i) \models \phi_2 \big) \land \big( \forall (j < i) (\mathcal{M}, s_j) \models \phi_1 \big) \Big) \bigg)$

Note that, for all paths ($\forall \langle s_1 \rightarrow s_2 \rightarrow \ldots \rangle (s=s_1)$), an $i$ has to exist wich satisfies the rest of the formula. This means that $i$, apart from the "rest" concerning $\phi_1$, needs to satisfy $(\mathcal{M}, s_i) \models \phi_2$, which requires a state $s_i$ in which $\phi_2$ is present.

In your case, this means that there has to be a state in which the output contains $b$; if there is not, the forumula $A[a U b]$ cannot be satisfied.