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

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

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$$.
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.