From 038181d1567cda3fb09b0f66eb88e745287f5393 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Mon, 5 May 2025 09:49:15 +0200 Subject: [PATCH] vault backup: 2025-05-05 09:49:15 --- .obsidian/workspace.json | 1 + .../notes/15 - A formal language for LTSs.md | 16 +++++++++++++++- Pasted image 20250505094841.png | Bin 0 -> 6253 bytes 3 files changed, 16 insertions(+), 1 deletion(-) create mode 100644 Pasted image 20250505094841.png diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 77179d9..e048ff4 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -213,6 +213,7 @@ }, "active": "cdcc59f1bf6d4ae1", "lastOpenFiles": [ + "Pasted image 20250505094841.png", "Concurrent Systems/slides/class 15.pdf", "Concurrent Systems/notes/15 - A formal language for LTSs.md", "Pasted image 20250505090959.png", 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 a4474ce..05cae20 100644 --- a/Concurrent Systems/notes/15 - A formal language for LTSs.md +++ b/Concurrent Systems/notes/15 - A formal language for LTSs.md @@ -56,4 +56,18 @@ Hence, $\forall \phi'' \in L(P'), \space \phi'' \in L(Q'), \space i.e. \space L( By contradiction, let us assume that the inclusion is a proper, i.e. $L(P') \subset L(Q')$. Thus, $\exists \hat{\phi}:\hat{\phi}\in L(Q') \land \hat{\phi} \not \in L(P')$. -Then, $\lnot \hat{\phi} \in L(P')$ and this would imply that $\lnot \hat{\phi} \in L(Q')$. This is a contradiction because $L(Q')$ cannot contain a formula and its negation. \ No newline at end of file +Then, $\lnot \hat{\phi} \in L(P')$ and this would imply that $\lnot \hat{\phi} \in L(Q')$. This is a contradiction because $L(Q')$ cannot contain a formula and its negation. + +### Proving unequivalences +The Logic approach presented so far is very natural for proving unequivalences: +- show one formula that is satisfied by a proc but not by the other + +It is not very effective for concretely proving equivalences: +- e.g. to show that $P \sim Q$, we should check that every formula in L(P) belongs to L(Q) and conversely +- the problem is that L(P) is infinite, for every P, it contains TT, TT^TT, TT^TT^TT, ... +- even if we restrict to logical equivalence class, the situation does not change +- EXAMPLE: consider process P2 ![50](../../Pasted%20image%2020250505094841.png) + - it satisfies ☐bFF, ☐cFF, ☐dFF, ... + - so L(P2) is infinite because so is the action set + +#### Sub-Logics diff --git a/Pasted image 20250505094841.png b/Pasted image 20250505094841.png new file mode 100644 index 0000000000000000000000000000000000000000..eb66d291b3d2d151c3dd1900d57860789c4b33fb GIT binary patch literal 6253 zcmb`MRa6vSyT%6?X^;j92~j#EBot6Oq+@7M(jkZL7@8quB&4KE1VJ3SVMys1>7f~c zK?DRD;&}e+TW78Ft##Hq7vIHR?|yIIt7kvIXYZY$r=vze%1jCX04Oxnl@0z@X8-^X zpBVq|F5mG^*xy3pscz;C08sY-_rl8%pkx66nAkOxUl;}C9p*21TcAQCCR%WmmIoYo zG-xgZI=)1>pjM-UTSAs}{mR39zei(+OL30yUHR73&^>naY5n2LX{5$}3fn^FCuAe< z)Vz)X9r6zM@6bV{)ziA|e)z+MPU=cBOjy)ZQfwCBV#OP~5Vq@I_=>4}r!DIJ1sjV+ zUZ5-FQBMRS%_T;)CcT)KMmL8~B0K(}yfEY7Qw$ z#xgwjXTf65QfbqS^iFKin~#eIbSlO@j1(-YVn6}l<%1&60Pe-zZasV`j}>dbGjvC# z_DlBn_i_!(Z#{v&hk5tzGgBH6Kc`@0GOsrOR8GSqlK&ag&a{F%U1d{{mL6DNnRD`m z@FHg@Jqnt9?23Gjm(?(>1l~F-{@ByFI2C*4~SKDnzy)wW_$w>(~UX1sPI>fB~%QX0Erm3fB5~&7UG6IP%KVg z$Xnx0{UbA}4UwB9&8sa&dkE(1HHr7PEt}W+hR$9NlpIMPm8zxi@G6whl1d$AZ>iguQ>qIo1N5y@ zseuxH&MSaYR+(e9$x3_R`p#7gi%iQp^O7IB%qqBm`Am#FMSg07yow8Cz=HVUD8%ys z^{(kccN|_?OPd3(OgnT)Aq94k><>0WU}ZQBEqFRCv!C zeJ`=(m`B~R!GOPRZPkpH5O-|81fQz8-U2tkU)(2LsX8$Jf5eci( zsfk(bBM@U|mI;k^x4~iM@h@M0y_3f|03byj3o%Y)g#pCGdA zZ#&=yvt8ECVNBI)@8x7=_g+yG7iJ(4`!O4f$eDs~9cQaCs?|aQIe7YXeHw|2!F$Nv@SnSO zVT}_StLNtw_acJaJDUBI(7qrdy}eiu_wT>g`pEd#@%D+6ZfEe-fyGfC>g;J|^tA6}F%epv z_8Ck0(`~G^N3m9{!8gZ57l_6Vk?C4pZbdVZ4n3w-Sc_DfdTPCJjfYe)u8#Ey6Y_VG z<*H?ZRae@C!rCMr464wXilT?aK59DAlKPzYXZ!P7n{?OfDry z9&goJf{jg;-0vY?mYbUyN|dY}#h=RD%L}s=At+JqyzOqT?b;xrJiiWmM#c$^id#{@ zBuZNux-6JJYW&)nJ(BgqrmN6;c;r_`M)C!?5&KY@au5rqCGT@KfgzI1>}3ihBREL! zH$@Fh>5zGbizYHEwhaLD6FrqeDT#dwwdNH4)~~!e@M6!8NPr#qq>r6nLAG6s-zQah z;p9QHzADL1-c2+ad?F-Rrr;k1pLzBWUhbRo2>ZvNSdJ}pJ7vmq_Sy6h&T;AwK7hJI z*ewhHWOYoy!Mi4rbZD@Xbugc-7&=Hj9FoOM6we_Ir2)wQ6p=jD@jnnaGX*WpUCiae zP^;Hls;-A7a!sw7A7QK+ogr5%%a;Q!`D!WH>l;|`9dfZX%M<&mOsi+t3XD4pj6?;= z2dm+G-QAT1;k@D2j26c6h50CgrBFIQYa8U`ncu^A);7<=vCBbUhyg!?a20))PjYLJ zj1!Dg-Ou;3?a;ZO?g943yq+}Ge+@Vu0k@J=Sf`A?WJ?s4PT`a7rrP&YBe&(vXT0zt zIdXXpa85*<(cm<56K$i#FK6Y|W~Hvp4dHkIZjEBzMfWC20)k4agA+nt^)MwTMZ8#_ zlPio%Lqp);_}=gOtO2!-_XcL2DHkQpqr2T*$87i0q=86j-R{k!yVECkzM9N;mZy3t zJw7-g>a~vLy3q^cfWn~)92W%C-UXisl=ucwhGZb&Z$jfdiv$EkdfZ|^R7Y7bFqBEJ zZW~m%;MKxCTOiM~zL`E+T)8sneKY964wE96h+1sZAro5W2d5vM1b~^PAV2t={T8!T zfvN5_Y#+i+Day;=E+AQM{a=fx)zV5|#6H@g&Xgv8oOFEdwsbP08+LGW@WuZXX2((X zgAg77nAH^?;AM~Msh5j8KVtHv*;8T-96d8|*t|M(X&CgVL3*h+=!NkJSu*GqN;JR~ z2;x!{^OVs_e1a>1122H+Vh`tEF$JyAr8vu@P|uLxL7OMYcQ<>D9ctE3{SFq6*m5AY zZ^J6tt0k&qwqY&_79h?=;ZIS$m)U=o6kZReCh8taF~x?cBgp+kXF&~3{Er_d5A0`mSolHIeY*Wum{2lJ-wn>;({!=KFQF; z11RgWGBa}x<33NF5?gTBF1Rv~#*FX2`p({q49*s!;n6UtnZM^n0{s~fzyHT+tfcp! zk^gJ{f2fgT2vj52c4K(=$JI|#A5IrRLpN%`Iw2E+_kxO*`C#HoEH(YemQjz6P{_pu<&o@f%UKc6LP{z+cvN#YP;RwQ9esBk?--aV zZRO6Nq0EJ9Pjgb~@(7vbnT+O?1h+(MdfBhNH$($1kL;5gzNN@%#m{VI8fj+Gw?0p4 zfQ}B@Nt2eD^K~^AQZe0Qb2NiX7#T|$SuE!>0hj@d95WMe^3*EcN(a=Yw}(xcgKy9* zpNDXNZ5YF6iP1#kZ)S?D%8+P#vlRbhL8HZFgUQ*lyD}T5xjwYM*)r;*pOx#OPV{tpae029 zCJs#wjTsn>OVZ>@sW)bOt}dfA)wvFMha%OUo?$;ejj@tAMwc4t=1Bwe098GhzMHg; zvBr*G13y|LS`nu@bx#bJA0o?c>`xnm05uR8gku9))L;>SI=41A8(|T2Jkx8dpK8_AQ=Bg%m0Vg;Minf@_3b)Do>2ql{xb^(e)>_ zJso&})g1G%YiEd%V{-=qqzcP?D@|i-fj&XZ+>Md{19s8qEw9Eux~T5l*7$m#mu0l z$3hHo8)`vqT)R8F!g(Pl3OB)z8TMJXCxgpsaxt#d)58$O{yBbx7mqM93Ou%wT`N(l zDUa}!%$Q(oCLSl&p+U@wos`smq>3t45EcFPLu=Do;VkzqW0n*w-;P-}?z}Y1QFn;A z;c%|tZtCHIll};UKM|D!a00zG^K8ssIPV)$ivLSFFT%3c(@|JxbgTaQDIq@BZ_)9U zz~xH__x?}HLx>)$sjS7Q>yE{jS$-$7ZQV?x1$64m^YfP0fSWf>n4Khf%@J6&9 zGB^6Jc+JhGWltDCOb)Nu&m^%Fk9eAmn@0*@frl(G5VatW~HTt#ow8 zn6lXFTZa&?9~3y*?8V@m+BIKI&%olR>coo}W!Vx9F)3!cs0|clBv!Ijn3B`%<-xg_ zGy9?uu|8LaF!N?>@FLcZlX8Q6glJjteyKyU7jODrp%zQYUS_ znUxJ*cxhJvw}*fDES5_8j|rO`rZ9mmK<0BfMp^a*8$gu?eBF&b_Hgv2oq!I?NZZ{+ z^N-?_{4o%0E;GeILZrF<{^zA_NCMqzwU*@yJr9a3CZmPc$uay4+mgvWn&|kP4k-%d zK4-gLPea{+xw>PONlzcGP&+xBSEnzSUR}%%`>);ZT@V%g@OPIG5-`doeGupO%QYG) zTRknO=KoqvqAcIWywhtZt4lu20dgqp0*FAuvSt#b@(iT z*$d4XBU>Ygafqe=)W>b_gcwAC*F!6pM&rpSA1%v=S^Q2LAD3kUukJHZD2;J@|3Mfb z9AG$7su!L>PFZTtyWNu%+DE{VGme!YK_y_MI*;d1JX9goYuRoHC& z1gcfsz5ncY@4kX;P{1Ra<74UQ4pUGYeHw{qoWCb-s*5hPgc_A_x2h$O4TcA}ET$EY zvz7}9xSiT94uP^|G~%Q8!n|zN<1=B&k7L>O{G%veFnB}@ArA6O^3cuC zEn{RC$?X0&SRNMU26e20eN`!eFFaY}euuSBGbD`eo>Uo;0yq+1OE4plp%%=^szrKx zA@^f3tq#+a<~DiU8gpQJK=;YjCg-?2>&w?L@dTl9?ndc%-#7jPO`757r18vNaJ{uK z9T*-E3uRZldOaj<#T4ThNaGQAne88C2xvY~n)>Ywqbx=E`uQ8P83Ap=e@c z_II#>0KJRQejYK{0YVH=zuohL8Wgjy>cQQ3lqR_;1(Q_zeMQsD`RDex;txtgbmCwb z*QKw53^Y7a{K<+R?E{!gTGNY?`s*2I)0#06K zb7KQT-gZ+_IJE}^VOD7@&C6h(8HA%2V$np-g)Y2{m|lJ2ap~MEJ}{8T}@cwhfFe{(@YOj)xjb6b0mpqcErvu$N0Ai0ZF_=A$!ZYr_72oD?Yt+z7ujLAH25K#@{;ZALu}n#e^Gio z`l%yfX3lzbeaw$Ct@w5^5!FX`uf`Nu^HQ*s^$g!8oJb&m*Hm^7o;r%=jX3+Lh<(kc zr40Yx73woNYMA*_B+hI{UkliDNSQRwTa#IiA=W5i0&CdK)A+LxbE;BR;sFv(-Hbfm zKmY(>!!oFqhoP2ye&FAv|2K#Ji`}IzD?UmyK1y@sz!#zi*i*sQa!d}P-dAxs_xglJ zwH$71&|J{7cLG+{;?LwKuvK+oP9fTy)LJz)>!A;lnkEKcecj&iXE!#Mlu#08G^}oL zQfLivc)Vs*CIYG=uc^_BIosZ^SPc(<UEi~L0GFI+5_UUdI#l^b78asf z4TssReajTkUgJLe+02_>cX2fpx;K6p%Ug;c8JPyMVLtyeycW{j+^#Pw`{pzm%-JCk ztf>0F9u@Xjtg)fs1>e3lES#kkq{}hZrnq$O&25o~D|{QD;h>#Xy|-(v*op~AH9Cz<{!46!s<9(ICjTJKvVHw zN`1TkBYSpX&tRb8udU(Bk}@iNCaerM569GPv&k@bmjyqW$A_>!z+}_IX%zBMEEd zoHAFo>#*BvTp`cFc5riMm=5Yl774=+0VyKk8jcM?TI;db;}H%16A!-gLx_i8*M^BC z|F+Z4rdleUK-yX!6>zPbsl1FA=iTv#C`agjj4#xqj8v{+M4aVgZU~s+0P4WV;|r2r z4GxKv2kIhH6-^6J2X8t+Vi7Tst{!t-{U;%;1^!crB@_Q7FeYAlx0|Z8;whI+ok}G0 z)bL82!x#Y%fzpypD`>(f6!;h2-unnI`4S?M`Fm$G+^Z)J?y&xE0Y3rdq&@EB|@(@x))d zy+(DNS19BkY!X^_EZ)N!5J#6wo?y=QD|GS#cB8zVtwgr==hjHhi}lt_}Jp?{&f z_h@btLe80%#nrd;h%g`pn|uiMkL)}iV6h6YAf_fqs!s{XUUR8%C4S6s(FR1!EGcyE z4y7?#U%^nRY>Sf8=p9c1NBTf}>TKd}pnt#txg^uA*)B!i(qAtk9Q0?qn(B$d zQL???5dB_FP>UT0u;dhJ{yjx+MYgmMULA%Tys`ex1n#MO5E)VD9%aEbhTtE|+;R)_ ib@=~pz}lwV5?yUpUxtw7ZT$T|0BES_DAy|5LjMb#vlp-c literal 0 HcmV?d00001