Are two CCS processes equivalent with respect to weak bisimilarity if and only if they satisfy exactly the same set of HML formulas?
(This probably does not fully answer, but I think it can still help)

According to their Def. 4, there is no modality $\langle \tau \rangle$ in their HML logic. Their syntax only allows $\langle\!\langle u \rangle\!\rangle$ where $u \in A \cup\{\epsilon\}$, and $\tau$ is assumed not to be in $A$ (Def. 1), hence $u\neq\tau$.

Also, there seems to be no recursion allowed in their logic.

Further, as far as I can see, in the Concurrency Workbench &lt;a&gt; indicates a strong possibility, while &lt;&lt;a&gt;&gt; indicates a weak possibility.

I can't recall which variant of the HML logic precisely corresponds to weak bisimilarity, but I think that it can't involve a strong &lt;tau&gt; modality since otherwise we would distinguish lol and tau.lol.