Model Checking CTL* algorithm
The algorithm is full and correct. If you look back to definition 6.80 in the same book, you will see that the until operator is part of path formulae, which in the CTL* MC algorithm are checked via a standard LTL model checker as written in the last switch case ($\exists \varphi$). The $\varphi$ stands for any path formula.

The algorithm also states that you take the negation of $\varphi$. So then you need to take the complement of the satisfaction set.