vault backup: 2025-05-05 10:04:15

Concurrent Systems/notes/15 - A formal language for LTSs.md

@@ -90,3 +90,9 @@ indeed, P1 can simulate P2 and viceversa, but the simulations are not bisimulati
 
 ##### A negation and conjunction-free logic
 ![](../../Pasted%20image%2020250505095743.png)
+
+### A Logic for Weak Bisimilarity
+Very similar. $$\phi := TT | \lnot \phi | \phi \land \phi|\ll\gg a \phi \quad where \space a \in Action$$
+The only difference is the diamond operator, that here is turned into <<>>a.
+
+This is very similar to the difference between the definition of weak and strong simulation, where the former is obtained from the latter by replacing $\xrightarrow{a}$ with $\xRightarrow{\hat{a}}$. Satisfiability of this new operator is expectable: $$P \models \ll\gg a\phi \iff \exists P' : P \xRightarrow{P'} \land P' \models \phi$$