From 830289beeb9498ac89aade3fb2d50eb25f1972f3 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Mon, 5 May 2025 09:32:04 +0200 Subject: [PATCH] vault backup: 2025-05-05 09:32:04 --- Concurrent Systems/notes/15 - A formal language for LTSs.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Concurrent Systems/notes/15 - A formal language for LTSs.md b/Concurrent Systems/notes/15 - A formal language for LTSs.md index 5624694..44b0d13 100644 --- a/Concurrent Systems/notes/15 - A formal language for LTSs.md +++ b/Concurrent Systems/notes/15 - A formal language for LTSs.md @@ -48,7 +48,7 @@ To simplify the proof, let us modify the set of formulae by allowing conjunction (<=) We prove that $$R \triangleq \{ (P, Q) : L(P)=L(Q) \}$$ is a simulation; this suffices, since the relation just defined is trivially symmetric (so is a bisimulation too). -Let $(P, Q) \in R$ and $P \xrightarrow{a} P'$. Let's consider $$\phi \triangleq \phi' \space where \space \phi'\triangleq \bigwedge_{\phi'' \in L(P')}\phi''$$ +Let $(P, Q) \in R$ and $P \xrightarrow{a} P'$. Let's consider $$\phi \triangleq \lozenge a \phi' \space where \space \phi'\triangleq \bigwedge_{\phi'' \in L(P')}\phi''$$ By construction, $P \models \phi$, hence, $Q \models \phi$, because $L(Q) = L(P)$; then, $\exists Q' : Q \xrightarrow{a} Q'$ such that $Q'\models \phi'$. We proven that the formulas satisfied by P' are all satisfied by Q'