From cf18a81e308e7080b4f322ec5f78d17705e47236 Mon Sep 17 00:00:00 2001 From: Francesco Mecca Date: Wed, 10 Jun 2020 12:46:44 +0200 Subject: [PATCH] esame alle 15 --- ...983fbc72a7cd009dabdf26995f474fa11d6e16.png | Bin 0 -> 170 bytes anno3/vpc/orale/preparazione.org | 36 ++++++++++++-- anno3/vpc/orale/ripeti.org | 47 ++++++++++++++++++ todo.org | 14 +++--- 4 files changed, 85 insertions(+), 12 deletions(-) create mode 100644 anno3/vpc/orale/ltximg/org-ltximg_24983fbc72a7cd009dabdf26995f474fa11d6e16.png create mode 100644 anno3/vpc/orale/ripeti.org diff --git a/anno3/vpc/orale/ltximg/org-ltximg_24983fbc72a7cd009dabdf26995f474fa11d6e16.png b/anno3/vpc/orale/ltximg/org-ltximg_24983fbc72a7cd009dabdf26995f474fa11d6e16.png new file mode 100644 index 0000000000000000000000000000000000000000..b882856aa5ce97eb55f103915135764955c975d3 GIT binary patch literal 170 zcmeAS@N?(olHy`uVBq!ia0vp^>_E)M!VDz;D$H~RQd$8%At3toyU)3K1-^a(J$)1H z>>cOMUnDQDaQfV(xcJ01>o(TbH}UcD-?{&|?)10wK-HWD9+AZi417mGm~pB$pEOWV z&C|s(ghMttA;2stA%T-4IblV@g_MLD$2QDqRGjs^iIKVc<2hyqM`6~lp=JNlfI1jF MUHx3vIVCg!0C)Q~P5=M^ literal 0 HcmV?d00001 diff --git a/anno3/vpc/orale/preparazione.org b/anno3/vpc/orale/preparazione.org index 58357a4..cb9c6a6 100644 --- a/anno3/vpc/orale/preparazione.org +++ b/anno3/vpc/orale/preparazione.org @@ -133,7 +133,10 @@ Legge del comportamente ciclico: | ∃m₀, ∃σ∈L(S) | mₒ[σ>m₀ ∧ σ=x * 2.1 Algebra dei Processi Descrizione astratta di sistemi concorrenti e non deterministici. -Si focalizza sulle transizioni eseguite piu` che sugli stati raggiunti. +Si focalizza sulle transizioni eseguite piu` che sugli stati +raggiunti. +Un processo e` composto da termini interni (sottocomponenti) e puo` +interagire con l'ambiente esterno. ** CCS: Calculus of Communicating Systems - A, B, C: agenti - a, b, c: azioni @@ -143,7 +146,7 @@ Grammatica: | E := nil | (E) | a.E | E + E' | E‖E' | E\L | E[f] ** CSP: Communicating Sequential Processes Due primitive: eventi (azioni) e processi. -| P := STOP | skip | a → P | P + Q | P ⊓ Q | P □ Q | P ‖ₛ Q | E / a +| P := STOP | skip | a → P | P ⊓ Q | P □ Q | P ‖ₛ Q | E / a A lezione abbiamo visto: | P := nil | a.P | P + Q | P ‖ₛ Q | E / a ** Structural Operational Semantics @@ -373,20 +376,35 @@ trace decorate: stessa sequenza di azioni e una volta eseguite stesso insieme di azioni possibili bisimulazione: stessa sequenza di azioni e ricorsivamente stesso comportamento +- Trace: + due automi sono ~ₜ se generano lo stesso linguaggio. + Nel caso di PA, due proc sono equivalentiₜ se possono produrre la + stessa sequenza di azioni. + dati p,q: + + p $\underrightarrow{a}$ p' implica ∃q' | q $\underrgightarrow{a}$ q' + + q $\underrightarrow{a}$ q' implica ∃p' | p $\underrgightarrow{a}$ p' + - Failure: definisco Fail(P) = (σ,X): dopo aver eseguito σ, tutte le azioni in X non possono piu` essere abilitate. - Simulazione: ∀p,q⊆P×P - p ~ q iff ( ∀a: p $\underrightarrow{a}$ p' → ∃q: + p ~ q iff ( ∀a: p $\underrightarrow{a}$ p' → ∃q': q\underrightarrow{a}$q' ∧ p' ~ q') - Bisimulazione: ∀p,q⊆P×P - p≈q iff ∀a: p $\underrightarrow{a}$ p' → ∃q: q $\underrightarrow{a}$ q' + p≈q iff ∀a: p $\underrightarrow{a}$ p' → ∃q': q $\underrightarrow{a}$ q' and - ∀a: q $\underrightarrow{a}$ q' → ∃p: p $\underrightarrow{a}$p' + ∀a: q $\underrightarrow{a}$ q' → ∃p': p $\underrightarrow{a}$p' ** Congruenza La bisimulazione e` una congruenza, ovvero B≈ᶜC → A≈A[B/C] +** Observational equivalence +Prendiamo due processi P, Q e un osservatore R. +osservare P e Q significa avere R in interleaving con P e Q: +| P‖ₛR e Q‖ₛR +| P→ₐP₁; P₁→ₑ +| Q→ₐQ₁⊓Q₂; Q₁→ₑ; Q₂→ₕ + * Fairness - Absolute Fairness: GF(exᵢ) un processo puo` essere eseguitp infinite volte. @@ -399,3 +417,11 @@ La weak fairness e` piu` stringente perche` richiede che da un punto in avanti il processo rimanga in stato di abilitazione. La strong fairness rilassa questo vincolo "e si accontenta" che il processo vada in stato di abilitazione prima di essere eseguito. +* Automa di Buchi +A = +- S: insieme degli stati +- ∑: alfabeto +- Δ: ⊂ S×∑×S +- F: multiset stati accentanti +run accettante: lim(run(A))= {q| q si ripete infinite volte} +∀Fᵢ∈F: Fᵢ∩lim(run) ≠ ∅ diff --git a/anno3/vpc/orale/ripeti.org b/anno3/vpc/orale/ripeti.org new file mode 100644 index 0000000..1fcd51c --- /dev/null +++ b/anno3/vpc/orale/ripeti.org @@ -0,0 +1,47 @@ +Rete di petri: grafo bipartito, Sistema: stato composito +Rete colorata: cd: P∪T → C, Post[p,t]: cd(t) → bag(cd(p)) +| Transition system: +* Semantiche: +** Peled: (Induzione Strutturale) +σⁱ il suffisso sᵢ, sᵢ₊₁, ... (σ⁰ = σ) +| σⁱ ⊧ p, p is proposition if sᵢ ⊧ p +** Katoen: +Diciamo che R⁰(s) = s, Rⁿ⁺¹ = R(Rⁿ(s)) +| M,s ⊧ φ if ∀σ| σ₀ = s, σ ⊧ φ (ogni path che parte da s soddisfa φ) +| M,s ⊧ p if p ∈ L(S) +** Katoen CTL: +| Pₘ(s) = {σ ∈ Sʷ| σ₀ = s} σ path - sequenza di s +Per induzione strutturale su ϕ: +| M,s ⊧ p iff p∈L(S) +| M,s ⊧ ¬φ iff ¬(M,s ⊧ φ) +** TCTL +CTL + Formula clocks, definito su TTS. +D = set formula clocks +| ϕ ::= p | ¬(ϕ) | ϕ∨ϕ | E[ϕUϕ] | A[ϕUϕ] | α∈Cstr(C∪D) | z in ϕ +Dati s = (l,v), w∈V(D): +| s,w ⊧ p if p∈Label(l) +| s,w ⊧ α if v∪w ⊧ α +| s,w ⊧ ¬ϕ if ¬(s,w ⊧ ϕ) +| s,w ⊧ ϕ ∨ ψ if (s,w⊧ϕ ∨ s,w⊧(ψ) +| s,w ⊧ z in ϕ if s,reset z in w ⊧ ϕ +| s,w ⊧ E(ϕUψ) if ∃σ∈Pₘ(s), ∃(i,d)∈Pos(σ): + | ∀(j,d')≤(i,d) σ(j,d'),wⱼ ⊧ ϕ ∧ σ(i,d),wᵢ⊧ψ + (dove wⱼ = w+▵(σ,j), wᵢ = w+▵(σ,i)) +| s,w ⊧ E(ϕUψ) if ∀σ∈Pₘ(s), ∃(i,d)∈Pos(σ): + | ∀(j,d')≤(i,d) σ(j,d'),wⱼ ⊧ ϕ ∧ σ(i,d),wᵢ⊧ψ + (dove wⱼ = w+▵(σ,j), wᵢ = w+▵(σ,i)) + +σ e` una RT trajectory: sequenza infinita di stati +| σ = s₀ →δ₀→ s₁ →δ₁→ s₂ →... +| pos di σ = coppia (i,δ) +| loc(i,δ) = lᵢ +| val(i,δ) = vᵢ+δ +| state(i,δ) = (loc,val) +** Automa di Buchi +A = +- S: insieme degli stati +- ∑: alfabeto +- Δ: ⊂ S×∑×S +- F: multiset stati accentanti +run accettante: lim(run(A))= {q| q si ripete infinite volte} +∀Fᵢ∈F: Fᵢ∩lim(run) ≠ ∅ diff --git a/todo.org b/todo.org index aa56e6e..57a266d 100644 --- a/todo.org +++ b/todo.org @@ -1,13 +1,13 @@ -* TODO VPC [23/24] -- [-] Teoria [31/36] - - [ ] PN consistente? - - [ ] vedi perche \neg\models != \models\neg +* TODO VPC [24/24] +- [X] Teoria [36/36] + - [X] PN consistente? + - [X] vedi perche \neg\models != \models\neg + - [X] fai buchi + - [X] Vedi step semantic e enabling degree - [X] Pronuncia / nome P_m(S) - [X] In ctl come dico: M,s ⊧ φ if ∀σ| σ₀ = s, σ ⊧ φ (ogni path - - [ ] ripeti fairness - - [ ] fai buchi + - [X] ripeti fairness - [X] fai equivalenze - - [ ] Vedi step semantic e enabling degree - [X] Come metti a parole \to ? - [X] Hierarchy of equivalences - [X] Automa di Buchi