Are two CCS processes equivalent with respect to weak bisimilarity if and only if they satisfy exactly the same set of HML formulas?

Question

I was skimming this recent paper and I was struck by the following statement:

two processes are equivalent with respect to weak bisimilarity if and only if they satisfy exactly the same set of HML formulas

I have trouble believing it.

I reason that:

1. weak bisimilarity does not account for tau-transitions and therefore is oblivious to the possibility of livelocks.
2. I believe the possibility of a livelock can be represented in HML,

and, therefore, a counterexample can be constructed.

Consider these processes:

One = lol.One;
A = lol.omg.A + zomg.A;
B = 'omg.B + 'zomg.B;
Two = (A | B) \ {omg, zomg};

Consider, furthermore, the HML formula

Livelock = max(X. <tau>X);

I believe that this formula is satisfied only by Two, which nevertheless is weakly bisimiliar to One.

I have tried to use the Edinburgh Concurrency Workbench to confirm my reasoning:

agent One = lol.One;
agent A = lol.omg.A + zomg.A;
agent B = 'omg.B + 'zomg.B;
agent Two = (A | B) \ {omg, zomg};
prop Livelock = max(X. <tau>X);
****** 
echo "Is One strongly bisimilar to Two?";
strongeq(One, Two); ********************* outputs "false"
echo "Is One weakly bisimilar to Two?";
eq(One, Two);       ********************* outputs "true"
echo "Is it the case that One |= Livelock?";
checkprop(One,Livelock);  *************** outputs "false"
echo "Is it the case Two |= Livelock?";
checkprop(Two,Livelock);  *************** outputs "true"

So, is it the case that two processes are equivalent with respect to weak bisimilarity if and only if they satisfy exactly the same set of HML formulas?

• If so, why is this true, and what's the flaw in the counterexample, above?
• If not, what did the authors mean or what sort of context am I missing? (Or was it a typo?)