Modello che controlla l'algoritmo CTL*

Question

Attualmente sto cercando di capire l'algoritmo di controllo del modello CTL* questo libro. L'idea di base è chiara per il fatto che possiamo usare l'algoritmo LTL ogni volta che abbiamo una subformular $ E phi $ o $ A phi $ Ma ho ancora una domanda che non riesco a capire:

Perché non c'è caso per $ phi_1 u phi_2 $ In questo algoritmo? Ovviamente possiamo scrivere la modalità fino a una modalità di rilascio, ma questo caso non è neanche qui. Quindi questo algoritmo è incompleto o mi sono perso qualcosa?