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