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

Question

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

Answer 1

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$...

Answer 2

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.