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?)

Answer 1

(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 <a> indicates a strong possibility, while <<a>> 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 <tau> modality since otherwise we would distinguish lol and tau.lol.