Due processi CCS sono equivalenti rispetto alla bisimilarità debole se e solo se soddisfano esattamente la stessa serie di formule HML?

Question

Stavo scremando Questo recente documento E sono stato colpito dalla seguente affermazione:

Due processi sono equivalenti rispetto alla bisimilarità debole se e solo se soddisfano esattamente la stessa serie di formule HML

Ho difficoltà a crederci.

Lo ragionare:

1. La bisimilarità debole non tiene conto delle transizioni tau e quindi è ignaro della possibilità di livelocks.
2. Credo che la possibilità di un Livelock Potere essere rappresentato in HML,

e, pertanto, può essere costruito un controesempio.

Considera questi processi:

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

Considera, inoltre, la formula HML

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

Credo che questa formula sia soddisfatta solo da due, il che è tuttavia debolmente bisimiliale di uno.

Ho provato a usare il banco di concorrenza di Edimburgo per confermare il mio ragionamento:

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"

Quindi, è così che Due processi sono equivalenti rispetto alla bisimilarità debole se e solo se soddisfano esattamente la stessa serie di formule HML?

• In tal caso, perché è vero, e qual è il difetto nel controesempio, sopra?
• In caso contrario, cosa significavano gli autori o che tipo di contesto mi manca? (O era un errore di battitura?)