From adfd49d3e8514ea47bff447971b76aac403bd8e8 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Mon, 5 May 2025 09:54:15 +0200 Subject: [PATCH] vault backup: 2025-05-05 09:54:15 --- .obsidian/workspace.json | 4 ++-- .../notes/15 - A formal language for LTSs.md | 17 +++++++++++++++++ Pasted image 20250505095249.png | Bin 0 -> 10475 bytes 3 files changed, 19 insertions(+), 2 deletions(-) create mode 100644 Pasted image 20250505095249.png diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index e048ff4..60dd8cf 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -213,9 +213,10 @@ }, "active": "cdcc59f1bf6d4ae1", "lastOpenFiles": [ - "Pasted image 20250505094841.png", + "Pasted image 20250505095249.png", "Concurrent Systems/slides/class 15.pdf", "Concurrent Systems/notes/15 - A formal language for LTSs.md", + "Pasted image 20250505094841.png", "Pasted image 20250505090959.png", "Pasted image 20250505090603.png", "Pasted image 20250505085454.png", @@ -234,7 +235,6 @@ "Concurrent Systems/notes/13 - Weak Bisimilarity.md", "Pasted image 20250430192526.png", "Pasted image 20250430183304.png", - "Pasted image 20250430175412.png", "Concurrent Systems/slides/class 13.pdf", "Concurrent Systems/slides/class 14.pdf", "Concurrent Systems/slides/class 12.pdf", 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 05cae20..e9a639e 100644 --- a/Concurrent Systems/notes/15 - A formal language for LTSs.md +++ b/Concurrent Systems/notes/15 - A formal language for LTSs.md @@ -71,3 +71,20 @@ It is not very effective for concretely proving equivalences: - so L(P2) is infinite because so is the action set #### Sub-Logics +Let's consider the sub-logic without negation: $$\phi := TT | \phi \land \phi|◇ a \phi \quad where a \in Action$$ +*Remark:* the formula ☐aFF is not expressible anymore. +Hence, we can only express through formulae what a process is able to do. + +Let's call L(P) the set of negation-free formulae satisfied by process P. + +##### Theorem +P simulates Q if and only if $L(Q) \subseteq L(P)$ + +*Proof:* The proof is similar to the one for the previous Theorem. The main difference is in the (⇐) implication, when φ = ⋄aφ′, because here we do not prove that the inclusion cannot be proper (indeed, in general it is not). + +An easy corollary of this result is that there is a double simulation between P and Q if and only if L¬(P) = L¬(Q). + +*Example:* it can be checked that L(P2) = L(P1) +indeed, P1 can simulate P2 and viceversa, but the simulations are not bisimulations. +![300](../../Pasted%20image%2020250505095249.png) + diff --git a/Pasted image 20250505095249.png b/Pasted image 20250505095249.png new file mode 100644 index 0000000000000000000000000000000000000000..9fdbed0e2a7c9b2d997c4897cdcbcc33c49f28dd GIT binary patch literal 10475 zcmb7qbyQo?vu>cc6(u7x7S-Q6X)ySuv-yZPP!-dk_2 zd*4~>Bqt}f_so3Xe0%nUsVd80qJ2OE005YBvXW{509*jY8K=)A(V>hCI_>S~JZ2>{z)qtNC8I66> zzZT@~%ClEjEcsi~(^p%9S5MBA`0nMZ7az(qw?fEBBQde6QNfg7=w^ad&t3B33hqHKT-9(tjTtGSay}s|*_zhz~72z{DMCUp1cZ5AiJiM1$jj?l+2F^wm zTY@D9qJmlPYo9yDq#1$8sG#oSJ8@n}XevvodKfiyxR_cL_T|Hni8Ng0e7u6FDPw%z73fIYxN zg5^C;V)Mbsim-Oeh&hFPOcXm)#b69R6^a64YZ#Kn)uTk=INxU4zv@yMO<=f0A&LzL z2YJ<%Y5;zO23nO9wK!hU&`@gnlt~Yf6wnk8ozHG4G{%&ObzZlH^>a{wZi>;i|Jp?H zZ*TJDo&4)RwXand7r>~4KUnVxP*9n4sXJA1!dVG-g4?k-6eoVv39hn<(NJ;(nG=VY zr1Wu3GKL!miBqdH?x@AZg73cLn^^I3_#`h2Po3C*hZIUn9@Fwa{bt3hj>e2h*)Oy9 zmRD8|0uqR$!JP>ddZsUx*F`OI21!{Z=#dJFgDo8R5EJs$UmKhtF zzGC_`m|ED_C*+3LY?)#fzki!1POE<3;d)?ic`f-FvbpY6BOj7`@dO~H&iiK{7*Kup z^04lEMe*joG>|6&v)=2LpB8Z8}AT<~`j*=%(>{c;z{jr!fN1 z%$gtKi)EE;qa;j{BZhW=z_LZKa^QJ z492*8-G6F9X82K`^bb8Q{hlB>K^y~)trF|{=EkZcyHkP71RwWmZkv_F`BSQDC;2L+?a5dK2N^9s?4P$98#ch=e}AysnU%rw~7!R=~h(v^kaTTxT+N-cqn zbIxPYP*@jJ4v&d?wE;8Xid#Z~*I4jmf08i~3%gwCSftKaId<=a^#ypOAQiPG*6lB? z(#Mwty%!k-965JnTt|xjXB{UA+ugDlN`My8b_OvACL}!gQYG&|4rgrQW{VH7|EzI* zxZbv6gKP7sb@{HviJA`jR1E{6Z5IzG_a{nRTtTKd+_;OeHxwz=NGWidg$|NGU8EmL zS2wd+l4yA+N3oCkkC=Z8KPGtGJouF`miS^a&=Lj8wuQWR4EY0D5DH9KInYD znB821@KedfOoSn3S6!jE`Mkp-MrhpTQc)Tm|L1(Pm1!QQOV`vG^d%vsLy(&3oU@IO zrjUoTpYn5CK~DQx7ZW=(FFoym%#lWQ{@prN$Qd$pLb21-#SO&D7C&sJHdHup0uI0W zI^J=qJU=4q`(-r~-efJf5DE^#Y9wOUMq;3gm}ha{r?Rl{ zaWsS2$`g`nc^esiF2L;&O%A}zlVnvdB0vaHjh_6c@Y43@F3*i=`-AU!ozv!`dH&aM zeqsWJZp!ik;}R(R6v_}2ntxf) zK}teYK;9pym?ibuRPlZIw?+2mG9;M4{?cIRUB;!vMCipD3J$8ra#d7G$0#n12j3QQ zA0a_|XR!$;2KuFBB)4$l#$V))?|tUxCKoIgf7#KVzvTvxzPs-iTfTj5>3Dh_Uw?fF zd`G73d&Td&E^z4hGl{FZr&4y}TMoQWP%sc4N@di3_jz>l{AFjb3RDQ z|0VtUS2Bxf`cVUz^;49wdVEsrbvw1@N;EQaNxO#0!^L?cc3+Y)CeBUBS(J;#4A0d0 zEuz>fC7I(AQ8T;CxYXsTVW!Z%0cuF8jXk6eCJCi9*8MHWDHG4-=(S_6 z&|omziFHhr$0H^npb9{NSAcysr<06LJLGPGbWJr>8oSpr^Wb~g+iexnvgE))D?=yN zT-)QZZ$|m+SoT>&0(x-v2|g+<^XXO^)v#&0_4DfZu@{bx5OXm)UQ**WxyixW?}M%E zWn)Ha9NdMMSFRwgD9%3%DOJ65a2KeI;VYMEl3yfQd#gwocq-?$lO{^3nfDdaXLyu^ zM1TbUB9(3uydkA6n>N?7l0Qs1rPkh#t9$n zTP*@TydelvC&=zNHsKDCQgrA!;IPGn$7sk6_CYmsqdqR&jzqL%J({S<30n3qjn8Hk zx8UAh7<%*0Z+!RwB)gE_Ev8lY8-gS;bKf7Us|N^ApWK!fL zt)6Cm0AL-cU!jM)CiuEFu^ChVLr`ZN!k;aRum049x0D`s2qjhXl6xHHXOlPOEhUve z6z>fLJaTX4f9iORkKdqP9D3WSPN~*DO;Q{=GyTNscpX40nf?{8U3Ffv?sF2yPHgAZ z2mBH?S3($Iuk1HBWy%w!;6PygN8WOr+zs3!`kejK4F*GI>^ z7rpg_8=i1m^0(VbU~?eFdwEbKf1n0`I&jh%kdgjbIO30;KO@!KOV=k&lGMaT4}kic zgWwumY}}mPmQLOW;ipv|JnS^4aNxFNYf_yx`M>5|R_W}Q$pkGm2K5HrSlz0z`G!&f z00SF%q<~J&|GuOQ0RTt?n=*w^f{J6Th`YF?PJWB*R zFAkU^2+dKs_GqJ_p(#|(tX{OiaLP{SwvCg|Cy%i-F#+YMCL|^r-?xo@@XIGAAwfrg zx2{_+AFK^7@N!TnSP|RELsE9tA zK_GY49YJbEUjGgYYiepL^qQ{LJkL`{_so4!0dtI@RJ|58nSxFQ<>hRGf=$K6%)Gpb zw8?LI92h+b^1FAZ%TA7t78VxKWI}wRqRQ-9@Q9t#4U?u;5J-JhRaIRbFB_XJH0fhe zQIP`0`+pd5adCZpeK6B#mE5knu9JQEaP{cLa_kJ+tq1Kl#REhHIZrhmQxxf%P1qHk?$&%|Mz{RL^Bvpv9F!}gq&(Bc{ zr_Z0e#xjM1L7U9uUsu7SjLFb-uj|pYv@})5+DIoSKUaV&WLF*G5J9lCm-p*RvJo1~@?00=SK;VOfNO!~SrJESFMPLhUQ&QWps3Of4_8iuDraw85gm(61*QC31bK;mJG}cGBQ60 zwwYL1prfOS&|N)#w74O&)YMd3IX;+c`S?tLNtu~tv(`IAJnv41pil`nX-aHK85!Swp>;v$gNeuM{Zoji zxp}@?QR@J$3GuKU@wtHa7U(=LF>x3}`j3OUi;F>!eDfAM4xrJ_>kwxp8lsZ%+>^ub zb|tgq?fY-V&>Lz+EaduZHu`(lAba4@IZMp z`d_esARr`MI=$=p`F{N`&UIgVy2D76zUURpr~SBq+}sg?HW01qL|1o^Jt}HpA)LYX zcZ@G%{^g?6358q!M^*$(D2pLp-LZPFDX@ zX(RUSt~0uf2BA>s(9oruFf0yWn6Pbly6%X&T(n>~QmH3M`k@lRKdidm%FhuBtj}X~ zNXlVkbVPWFsNn4VXM?`xhprMnlgnsLa(sX#f67&sz*QH$AThH)FtM{^rmj9cI4CPA z*}K-}xxKYDH^H@ASy`Ezo4d8O1q&f`A~u*s8}-V^AIbT4?%fIo0#J>0Q&Vn6Vxq>_ zZD) zlQheW?d|%>Z|sDxGwMP;v;vT1RI4O&GOPh8d&hrR)4;$$Q!`(KIj$~@GW6iUDpPrW zZO!NQNV86t3=hv~-Zu&@2n4dcXmu$5zB7#c&Xk+`n%v_+_n5NzoJEKm@5UshW_*`;bI-s^SqsuSw@OZJ3gU9G09BMgX;dAS!E6YY40>Z*xM>9+@ z12s2@|vn!R&pjHDr*dZa&Gc%*%;&KZMx3f70lfS>$dBu3o^+#yoqB)#9Ptj2| zC##GdtFYCq0%1{^H)^4vqO!jkK+wLHK!rjTf83p~`%Z!e7;Vg`z|Gp7E8vr?0Sg&e z&VYfG6?(Q*$MW&x5AT!kSXo*aBMU?~)YfJQxkl&y?d}F;D!V>)^rGZQk|pN;wnC8L z#Fqdk88Ze^av&Uy!i#R(VSEH};tz=0P+IMIeERgMxuu0TWUVgJKKE3j!-aDOVs)k z#bMp|Q0(nd_IS^%G)*2;SXNe6R3yhrXt!9MUs;K*`>px! z-$5e|aeePfNvdp9Td&HqKo)vCS-(l!7@5CO#m`s2tmCX^9j$)Eq;p_wJ2ovXEk%=y zFcU_Ul$6YyBdv;KOS-u|;Hd~3^L$udS{lm`+=jGl&Tv=Kvi=}DFZDid@Vz8azwA*F zy{`Kh>A5jjB{t%&ecP?O%voDmscLBW1~q);VrRF5iHf12p+OIZMEU#kbwgdjGHhh0e-k*^ir`xu>y&iaGianp7+j3dc3Pj7RX@ta&SY7H{{?YFI5S;_VJZyL{ zl$|Wr6c!gBNk>_lwY7Z7|NGw{?B2g_yIcAm7#Qf&k$nvD=VdzJ8Q1mZ2FrhLR+it2 zJ~XBX8H%5(b>onw8L=MCt(XOVASV~~eSKb70BdP!xwyDEJKxA>9QCL$hFkNbot&IZ zO-+eYs%mS`&(7XHLQCNqF(r`ULlcq;rJ)>fM`vvdazd?PlhvtvPIzakMs>C$b8FbV zO4G3Xo6K&Qm6a786;)PR3S%fqKJr9)mp@*&yU^tHw6uUOBQ32YP|ilPzR|}ny0i-p zr2xm`mKsyx#)(Dl!%I2DyP-V@GkcUpoMv+y*pw3=EqHHlPxN6U@bK{P`T4oJx>~6G z_aY_C+fq`&s*J);dy3xPB0U_BkB_)v2nFMvM6?-7aBC$mLTeOt7hre(-VtMn@2!;rFQG_aVRsP--;^wegt@?qAo{ z*6OuDqG*SPhlgQw8z+mqr5M@B~0N&3jj`dmu(2)ID1 zU^rn4uLiS@j*entVuEri^YUof+23;=*viI7Mn$c{bSD_RFfpNOYPvl#f-xTjZ}f2h zTWMOWq^_>+_F}WgqpiKU`4bCE#If`xS%~rG=H}D=xr)5}(cz&WjBlX30p@dl`wt`% zFqv%$gAL>aEG5;~?)_w9YT9HwnUgs|)Ik37~FbJ*+%Pm;uzrWMp51S7+A0On8 zBX()mS3;OqY2^$W?Q`1O$v?+tWRN!LVevPSz$rYnwfil{9J*Y6jro$}H^1ATCtn3H z9JMBYCM7Y^Niw%3+_BVwSXmwPhT(~bh^Po(O1irXnoV#GL!q7*UC1!SRpI+`JU2I& zzI;jK`>sT51g^9_*6GE5W?KV#KgivDCMBjxCjvi1v_C+jxLlHCcN*@R=HA7CUPWTE^Teq!%aIq7V!Pz zxRIVtQ#W;MSp4lBbr9%D@;q3g(5YBqWnO||2l$-=_}Vp&_4e19zdNQJ`zPlPiS3zH z%Y@wN8YxCFTUN)+>S~!<5gHm=e0;oYd{9?}IRidgl=L=iEkGP{cyfY)0KZs8oj!Xt ze7q0IKhu`i6mAwnh9b~lqJ~|X3-0(*d|xiQFGf6Bu}}WyA*u7~9Iwo#e_CcL+`@z| zNH2tBDO7lg@XqIOD|l>7xlUJKPcI`i6*aw23rjAZlao`(^-NJ-J}o1|=I}%1C#HhU zvM#xrp7#o*^E99jnF;MptrySB=P86IU9p87u9dEX_2-iVG>N!y^*N@YocFw#3$5zK zZYx~Qk5f{0x^3>)drIkiWrgbA52yo|2L}iGEs(x}f%MYXOC6b<+Wc}Cx0Mrr&RiF{ z+-NR(0%@g;tjq>*S%Ij!eJ@c>VW%vb8;?xaXN;%Ij$j?0oyTudsbK zYdbCtf)#T{J4(DZiq7AT(UU#tx49fCypKrWzO|NL^S{$ClSrbR$3$T9k7eXBe;Sry z*stKz=ax-j*DOGZ6QbxCOVn&fHL)6Yc-ZeC%go@CmOfaSuImuEhmQ`rSkb^fxrOyS1!-K(~KuTiZ?@nMPW5J_Ow><><8 zUe)97pl_R?=*bwf_CDPaPL|Fr@JfJ{j3~O*eebBdbo#jdKG;P4ip8~8hBj}9mZ7gt zGWc5_2VZS~Du{KK;dG55J5^EPh~k7IgFHLU^UdwNo2SXBU6;WV`j>{n=eHs&VGnDU zM*yni)dDNc6-YrgARMF0nyQ<-J8}q>>5|F4N$6fUJ{_kJ zA4gbcv}r5{$d+*Q2lwU+s!s4O+mf?G{O?nT9E8g6;A8 zSy=HLmn~(GLRy{(!|ybtOEjtBMH%K2!;*fru|s(nE zM*!t-{*LG>42fy{(MrY;JOQi*+wTZaE)1#35fhh;(Ibawg_EuI($-yA0#3hunLOK8v)smY6%T=9sto;J8&A#zad-EvBV4nO zNhlU#fo}B6L*JjW)jyxZr5pnA<8LS3N44mP4DSKL=L!;_91SUtfu2+S(~cbA!ZVGF~4eXzx}6m#>_u+n-~Niom|(iw!X^XHgB-Uk6xoNMgbYPCut5 z4(+HU_4U}LWrOZ6_t4MZb~+5&7VJ;w^kxQw7JHm0ae? zpEiaExKTdG?r}4))k9*wzCb61JCRvII=W*s`i=ItT1X$sjX8uSd|tbs>gI(p;A_gB zchX3jmo$8@reug~8_R};)eWzoLO$2@$WT4Q%ClFVquUY~-peYWbOy_PMZ$5lbR@R` z^TprhCM(7U56*PhPm$)O-)EF-RJF6SSLWP*F5VoXdK>LxJo(55CxwwN%8HXiivVkddJ(|H3Gnu-c><{B1E zJEB1J@$!TDJm?onvBsbV-&$F^AcK!YSNoyJ7jiZzpU+fBu_V4^N;B^$ku5yMP*tfV zx4NrT$>(>AJBQ5#nq`aQvMG8u3Jb}9+*Sw^dfw;?yuZ%`Qem^yqD4w^^q<`ctcb>GR24bTOBj0Z zZ64(&pdcE?6S5M78|8uM2*ME*CkX7vg}hkHm6#bTd`>1SNdK}$sa{n0VKypL#>@6{ z1p`o3U)@`TfVmj`dGW~P9yhRvUCsE5i&}YGSr}=~IPWa6x~RUN=FzXH7F_Q(faeJz zB&l;{J)E>mQX-E-{KvaPg!!f?7Jn5g8?;+H zx&KjjY&cuc){iT}{{8G8(>9#15^210<1oll4GF_BkXm|NnQs{}+4YU?M4_^N<{g^24mX zXb2t&d3wBh7CBrMG9a7dZt=4HjwR})CjDO6tM>XQ0DuzrpI(40!XK*P7qfP~!~O73 zRRicjlk4j`)Q+s;l<%_YnHE6u;kXWlrjD1G^|#mHH91ee^!tP1erz^ush!iM41Dbj zo5*OCuZ!hGfQ_t8oUo#=knVk`W7rpZ()PB{rLMy6QONlGt1ed{@1 z-A0cFWLO~q-g6jSmwvP1syzNau6e$qsR`VyVVlt>{R0lt=jW6}6bURlO7(e*5{Q+^9kgzj(&oA2 z$N}qI?3URXG_LrZ=6-O|snvYDyBPzQMf%~x`ynHQr;IdCI*#rdwkfNc(Iu57}h;j6W84=Gt?F;CdHNyPVi(r8~$r~qzoc;BYE`9-$wG1NiBu?cbd zX-!Nt@>F`e7NsXjl+v;PYKQmZ1Ms7$fo#~FNn8N8;E6tSn)gu|{u+3L+AC z*Q#nLfbuU{sa1bdidVOY7@8pZEAMt2ouVR#%kmT^xH8`ugc&P%l{$w?i)bk`2-v-2%Mia_D-o zLw>=BNelZ{ZCV?yM>iY{VJAR+}OnG-8DCz30>#o^*W+EpX+#Hgg|bVEiC!PY8gPV?hPuy13V3ZblhRJ7u1J34a>tQoL);yRD=in`HOD7jZNgK8LoKtcZL7}0!{vK>5pB$>66YnCPb#C zG@{XD&YbilDm+cjB4#-9l+5hwBYuYObRhCoCwKsgnvE=bQp?_m1tHPV6b-@PzX&Q2 z89^C7P_~yXIx6uGX=VT>ppiQP8?8ruiq=3Y&p1DX1GSqU>hLqvnnyR0N;inPml_{U z>0Kv3JOX+QkG$C?HHdo0nDfD$_%H6DWS)E(r3(@+qzJB4h%q3Phbu?1kYE^Jn3P8+ zi9W~SP{(j7CjEvE_!dA2@T0WqswXRV_UwJvJ`Pa z!3P|Gy$q|ww9kHPAAy;DoL-K`u++n+aH^z&lWCD#qKX?#mDNZp{l{pLBF;^D&i93g za0~VUw#PU2^Fz(j*8$v}8zxQEY)t0Y^+#@*DH}?@o3A|q`GKO#Ba7SYZ_sO*3M|D{ zkLN{Sx67|8XQL|7*p~%=aRDTFc+M(Vwe7b{zHh7S(d%iE;p2>McgVwbA{xcXal(t1 zzHeo}ThY16&b{sp4IkZ*s8Ft^VqUi;PZOE=HT)6%Onscj7w>)F8s6Mbw(++9c)y4} zb&2Vb*L`wVN4$GA9Xy9byYi~%Y!r5gE8RpXMe4DmqXRZ#XL*dtDV}fsMDia{*f#S0 za7B)-BbQ)};BY;;tjrOo#K!0zA_dq-nuG7KM94$T1IR0~3+8?7P^7^4ZPzhWgt)Xe zwa9+o54O^8u#SIy!B30`7Kko;1X9aZePX6plMENFi&2cjCLq8mAY_*~1^^T&wXB^# z1^Pe0G!P|SEfZ7KhoVsMH7BhWv08&@GXu8>lOhd0;yjBwo?{(V^G%5qqI=k8WfKM< z`Ws#~x;$*59X-u#&i_vo6emgYD-nFDD5aGrUH?$8e~pZQn)h#tESQDUsS)gh@(C1e7uA`d=RDabU93dn;CRDzJu!goOPK}B4)a>;18i4@(k8wq{A@+gF zbQ{pd3F-yo_b_hFrp5tOQvI*m?f!4kVTcwDsC;#^+!y&(