Qualche leggera confusione con l'operatore fino a CTL (ad esempio A U B)

Question

Ho disegnato un sistema di transizione molto piccolo in vernice che userò come esempio.

Voglio vedere se $ A (AUB) $ detiene per questo sistema di transizione. Dalla mia comprensione, questa formula CTL chiede se tutti i percorsi soddisfano $ AUB $. L'unico percorso che possiamo intraprendere in questo esempio è S0S1S0S1S0S1S0S1 ...

Questo percorso produce l'output (1) $ aaaaaaaaaaaaaaa ... $ o (2) $ aaaaaaaaaaaaab ... $

(2) Decide sicuramente - comunque è (1) di cui non sono sicuro. Ho ragione nel dire che $ AUB $ non è valido per (1)? Dal momento che possiamo continuare a loop su un infinitamente senza raggiungere la B (e perché (1) non soddisfa la formula, $ A (AUB) $ non è valida per questo sistema di transizione).

L'ho capito correttamente? Immagino che la principale confusione per me sia che esiste 1 percorso ma più di 1 possibile output.

Ogni aiuto è molto apprezzato.

Modifica: questo è il sistema di transizione a cui mi riferisco nei commenti qui sotto