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:
- weak bisimilarity does not account for tau-transitions and therefore is oblivious to the possibility of livelocks.
- 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?)