* Simboli: - sqcap: ⊓ - Box: □ - a\b: a̱ - Vert: ‖ - $\underrightarrow{a}$ (toggle latex fragment): $\underrightarrow{a}$ - varphi: φ - models: ⊧ - Delta: Δ - approx: ≈ * 1.1 Petri Nets ** Definizione Petri net N: 4-tuple. | N = - P = {p| p is a place} (state variables) - T = {t| t is a transition} (change of states) - → (Flow function) ⊂ P×T ∪ T×P - W: Flow → N⁺ Visualizzabile come grafo bipartito. ** Altra definizione Posso sostituire → e W con due vettori ∈ Nᴾˣᵀ | N = - Pre: funzione P×T → N; rappresenta gli input delle transizioni | Pre(p,t) = W(p,t) if (p,t)∈→ else 0 - Post: funzione P×T → N | Post(p,t) = W(t,p) if (t,p)∈→ else 0 Da Pre e Post posso generare la matrice di incidenza C | C: P×T → Z | C = Post - Pre ** Marking di una rete Definiamo Marking m (vettore ∈ Nᴾ) la funzione | m: P → N | m(p) = n: ci sono n token nel posto p ** Sistema P/N Un sistema P/N S e` dato da una rete di Petri e il suo stato iniziale (marking m₀) | S = | Stato composito: unione degli stati dei singoli posti L'evoluzione del sistema e` determinata dallo scattare delle transizioni. Una transizione puo` scattare quando: | ∀p, m(p) ≥ W(p,t) ∧ (p,t) ∈ → | m ≥ Pre[-,t] Possiamo calcolare il nuovo marking m' allo scattare di una transizione t come: | m' = m + C[-,t] | m' = m - Pre[-,t] + Post[-,t] | ∀p, m'(p) = m(p) - W(p,t) + W(t,p) Si scrive: | m[t>m' Posso definire postset e preset di una transizione o posto come: | •t = {p∈P| (p,t) ∈ →} (preset di t, ovvero al posto di • p) | •p = {t∈T| (t,p) ∈ →} (postset di t, ovvero al posto di • t) | t• = {p∈P| (t,p) ∈ →} (preset di p, ovvero al posto di • p) | p• = {t∈T| (p,t) ∈ →} (postset di p, ovvero al posto di • t) | ∀p∈•t, m(p) ≥ W(p,t) → t e` abilitata ** Sequenza di scatti La sequenza di scatti σ nella marcatura m e`definita come: | σ = [t₁, t₂, ..., tₙ], tᵢ∈T Scriviamo | m[σ>m' if ∃{m₁, m₂, ..., mₙ}: ∀i ∃mᵢ| mᵢ₋₁[tᵢ>mᵢ Possiamo dire (state equation): | ∃σ| m[σm' → m' = m + C•σ (integrale di C su sequenza σ) | ∃σ| m[σm' ↚ m' = m + C•σ (m non permette di eseguire σ) ** Linguaggio di un sistema P/N Un linguaggio L(S) di un sistema P/N e` definito come: | L(S) = {σ| σ valido per S in m₀} ** Reachability Set Il Reachability Set RS(S) e` definito come: | RS(S) = {m: ∃σ∈L(S)| m₀[σm} Il Reachability Graph RG e` generato usando come nodi i vari marking, e come archi le transizioni che collegano un marking al precedente. *** Proprieta` di RS e RG - Boundedness: definito il bound di un place come | bound(p) = max {m(p)| m∈RS(S)} | ∀p∈P, bound(p) < ∞ - Liveness: ogni transizione puo` essere eseguita infinite volte | ∀t∈T: ∀m∈RS(S) ∃σ| m[σ>m' ∧ m'[t> - Reversible: da ogni marcatura si puo` tornare alla marcatura iniziale | ∀m∈RS(S), ∃σ| m[σ>m₀ - Home state: un marking m e` detto home state quando | ∀m'∈RS(S), ∃σ| m'[σ>m ** Step Semantic Step s: multiset di transizioni s e` abilitato in m se: m ≥ Pre • s | m' = m + C•s La sequenza di scatti sigma e` ridefinita usando s *** Enabling degree Numero di volte che una transizione puo` scattare in parallelo eₜ(m) = max {k∈N⁺ | m≥ k•Pre[-,t]} * 1.2 Reti di Petri colorate Una rete di petri colorata e` definita come: | N = - C e` l'insieme dei colori - cd: P∪T → C (definisce il dominio di colore dei posti e transizioni) - Pre[p,t], Post[p,t]: cd(t) → bag(cd(p)) Una transizione e` abilitata quando in ogni transizione del preset i token di colore cd(p) hanno molteplicita` ≥ Pre[p,t](c) | ∀p∈•t, cd(p) ≥ Pre[p,t](c) | m ≥ Pre[-,t](c) * 1.3 Tecniche Strutturali ** Flussi Definiamo p-flow come un vettore: | y: P → Q | y.C = 0 Definiamo t-flow come un vettore: | x: T → Q | C.x = 0 quando non negativi: p-semiflusso e t-semiflusso Definiamo il supporto come: | ||y|| = {p∈P | y(p) > 0} | ||x|| = {t∈T | x(t) > 0} La rete si dice conservativa quando: | ∃y | ||y|| = P La rete si dice consistente quando: | ∃x | ||x|| = T I flussi sono canonici quando il gcd degli elementi non nulli e` 1. Un p-semiflusso o t-semiflusso si dice minimo quando il suo supporto non contiene strettamente il supporto di nessun altro semiflusso. Un insieme generatore Ψ_y e` un insieme del numero minimo di p-semiflussi, detti minimi, tali che e` possibile generare gli altri sommandoli moltiplicati per un k | ∀y: y = ∑ⱼ kⱼyⱼ, kⱼ∈Q, yⱼ∈Ψ ** Invarianti Legge di conservazione dei token: | ∀m₀, ∀m∈RS(N.m₀): ∀p ∑ₚ y(p)m(p) = ∑ₚy(p)m₀(p) | ∀m: ym = ym₀ 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. 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 - a̱, ḇ, c̱: co-azioni - τ: azione silente (τ=τ̱) 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 | E / a A lezione abbiamo visto: | P := nil | a.P | P + Q | P ‖ₛ Q | E / a ** Structural Operational Semantics *** Prefixing (assioma) ——————— a.E $\underrightarrow{a}$ E *** Mixed Choice Composizione non deterministica con scelte miste: ogni azione, τ inclusa sono offerte all'ambiente (solo le azioni visibili possono essere controllate). E $\underrightarrow{\mu}$ E' —————————— E + F $\underrightarrow{\mu}$ E' F $\underrightarrow{\mu}$ F' —————————— E + F $\underrightarrow{\mu}$ F' *** Internal Choice Due assiomi che mostrano che il sistema puo` evolvere in uno dei sottocomponenti. —————————— E ⊓ F $\underrightarrow{\tau}$ E' —————————— E ⊓ F $\underrightarrow{\tau}$ F' *** External Choice Come nel caso delle scelte miste, ma nel caso di un'operazione silente le sottocomponenti non vengono scartate. E $\underrightarrow{\mu}$ E' —————————— (μ ≠ τ) E □ F $\underrightarrow{\mu}$ E' F $\underrightarrow{\mu}$ F' —————————— (μ ≠ τ) E □ F $\underrightarrow{\mu}$ F' E $\underrightarrow{\tau}$ E' —————————————— E □ F $\underrightarrow{\tau}$ E' □ F F $\underrightarrow{\tau}$ F' —————————————– E □ F $\underrightarrow{\tau}$ E □ F' *** Evoluzione Indipendente E $\underrightarrow{\mu}$ E' —————————————– E ‖ F $\underrightarrow{\mu}$ E' ‖ F F $\underrightarrow{\mu}$ F' ————————————–– E ‖ F $\underrightarrow{\mu}$ E ‖ F' *** Evoluzione con sincronizzazione E \underrightarrow{a} E' F $\underrightarrow{\underline{a}}$ F' ————————————–––(a≠τ) (CCS) E ‖ F $\underrightarrow{\tau}$ E' ‖ F' E $\underrightarrow{a}$ E' F $\underrightarrow{a}$ F' ————————————–––($a\in{S}$) (CSP) E ‖ₛ F $\underrightarrow{\tau}$ E' ‖ₛ F' *** Restrizione (CCS) E $\underrightarrow{\mu}$ E' —————————–(μ,μ̱ ∉ R) E\R $\underrightarrow{\mu}$ E'\R *** Relabeling (CCS) E $\underrightarrow{a}$ E' ———————————— E[f] $\underrightarrow{f[a]}$ E'[f] *** Hiding (CSP) E $\underrightarrow{\mu}$ E' —————————–(μ ∉ S) E\S $\underrightarrow{\mu}$ E'\S E $\underrightarrow{\mu}$ E' —————————–(μ ∈ S) E\S $\underrightarrow{\tau}$ E'\S * 3.1 Linear Temporal Logic ** Transition System | TS = - V: insieme delle variabili - ∑: insieme degli stati - T: insieme delle transizioni: e → t (condizione → transformation) - I: condizione iniziale - R: S → S = funzione successore ** LTL: grammatica | φ ::= p | (φ) | ¬φ | φ ∧ φ | φ ∨ φ | φ U φ | Gφ | Xφ | Fφ Set adeguato di operatori: | {U, X} - X e` necessario - Fφ = true U φ - Gφ = ¬F¬φ ** Semantica di Peled Detta σ la sequenza s₀, s₁, ... e σⁱ il suffisso sᵢ, sᵢ₊₁, ... (σ⁰ = σ) | σⁱ ⊧ p, p is proposition if sᵢ ⊧ p | σⁱ ⊧ φ ∧ ψ if σⁱ ⊧ φ ∧ σⁱ ⊧ ψ (stesso per neg, vee) | σⁱ ⊧ Xφ if σⁱ⁺¹ ⊧ φ | σⁱ ⊧ Fφ if ∃j≥i| σʲ ⊧ φ | σⁱ ⊧ Gφ if ∀j≥i σʲ ⊧ φ | σ ⊧ φUψ if ∃i, ∀j=1, ..., i-1: σʲ ⊧ φ ∧ σⁱ ⊧ ψ # | σⁱ ⊧ φUψ if ∃j| σʲ ⊧ ψ ∧ ∀k| i≤k≤j σᵏ ⊧ φ ** Semantica di Katoen Data la struttura di Kripke M = (S,R,L): - S: set di stati - R: funzione successore (anche chiamata →) - L: S→2ᴬᴾ 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) | M,s ⊧ φ∧ψ if s ⊧ φ ∧ s ⊧ ψ | M,s ⊧ Xφ if R(S) ⊧ φ | M,s ⊧ Fφ if ∃j≥0| Rʲ(s) ⊧ φ | M,s ⊧ Gφ if ∀j≥0| Rʲ(s) ⊧ φ | M,s ⊧ φUψ if ∃j=0, ..., i-1| Rʲ(s) ⊧ φ ∧ Rⁱ(s) ⊧ ψ (induzione strutturale su ϕ) * 3.2 Computational Tree Logic | φ ::= p | ¬φ | φ ∧ φ | φ ∨ φ | EXφ | EFφ | EGφ | E[φUψ] | AXφ | AFφ | AGφ | A[φUψ] Insieme adeguato di operatori: | {EU} ∪ {AX | EX} ∪ {EG | AF | AU} Data una struttura M, definiamo un path σ = s₀, s₁, s₂, ... tale che | (sᵢ, sᵢ₊₁) ∈ R | σᵢ = sᵢ | Pₘ(s) = {σ ∈ Sʷ| σ₀ = s} Per induzione strutturale su ϕ: | M,s ⊧ p iff p∈L(S) | M,s ⊧ ¬φ iff ¬(M,s ⊧ φ) | or e and | M,s ⊧ EXφ iff ∃σ∈Pₘ(s)| σ₁ ⊧ φ | M,s ⊧ AXφ iff ∀σ∈Pₘ(s)| σ₁ ⊧ φ | M,s ⊧ EFφ iff ∃σ∈Pₘ(s), ∃i≥0| σᵢ ⊧ φ | M,s ⊧ AFφ iff ∀σ∈Pₘ(s), ∃i≥0| σᵢ ⊧ φ | M,s ⊧ EGφ iff ∃σ∈Pₘ(s), ∀i≥0| σᵢ ⊧ φ | M,s ⊧ AGφ iff ∀σ∈Pₘ(s), ∀i≥0| σᵢ ⊧ φ | M,s ⊧ E[φUψ] iff ∃σ∈Pₘ(s), ∃i≥0| ∀j=0, ...,i-1 σⱼ ⊧ φ ∧ σᵢ ⊧ ψ | M,s ⊧ E[φUψ] iff ∀σ∈Pₘ(s), ∃i≥0| ∀j=0, ...,i-1 σⱼ ⊧ φ ∧ σᵢ ⊧ ψ ** Comparing LTL and CTL | φ_ctl ≡ φ_ltl iff ∀M, M⊧φ(ctl) iff M⊧φ(ltl) Data una formula ctl φ e ψ una formula ltl ottenuta rimuovendo gli operatori di path da φ: | ψ ≡ φ ∨ ∄ (equivalent ltl formula) * CTL* (state) | φ ::= p | ¬φ | φ ∨ φ | φ ∧ φ | Eψ | Aψ (path) | ψ ::= φ | ¬ψ | ψ ∨ ψ | ψ ∧ ψ | Xψ | Gψ | Fψ | ψUψ * 4.1 Time Def: a clock is a variable ranging over r⁺. Clock constraints: | x < c | x ≤ c | α∈Cstr(C) | ¬α | α ∧ α The set of clock constraints over C is Ψ(C) or Cstr(C). ** Timed Automata Is a 7-uple: | A = - L: insieme delle locazioni - E: insieme degli archi ⊆ L×L - L₀: stato iniziale - Label: labeling function L → 2ᴬᴾ - C: insieme dei clock - Reset: E → 2ᶜ, assegna ad ogni arco il clock da resettare - Guard: E → Cstr(c), guardie sugli archi - Inv: S → Cstr(c), invarianti delle locazioni Definisco /clock valuation/ la funzione | v: C → R⁺ dove v(x) restituisce il valore corrente del clock x. | A = | reset(x in y)(y) = v(y) if y ≠ x else 0 | v ⊧ x≤c iff v(x)≤c | v ⊧ x - S = {(l, v) ∈ L×V(C) | v⊧inv(l)} - s₀ = (l₀, v₀), v₀(x) = 0 ∀x - → ⊆ S × R∪{*} × S: 1. (l,v)$\underrightarrow{*}$(l', (reset Reset(edge) in v)): + edge ∈ E + v⊧guard(edge) + (reset Reset(edge) in v)⊧inv(l') 2. (l,v)$\underrightarrow{d}$(l,v+d): + ∀d'≤d: v+d' ⊧ inv(l) *** Path Definiamo il path σ di un TTS come una sequenza infinita s₀ →a₀→ s₁, ... dove ∀i sᵢ→aᵢ→sᵢ₊₁ e` una transizione nel TTS. il tempo trascorso ▵(s,i) e` definito ricorsivamente come: | ▵(s,0) = 0 | ▵(s,i+1) = ▵(s,i) + aᵢ if aᵢ∈R⁺ else 0 (aᵢ = *) σ si dice time divergent se lim(i→∞)▵(σ,i) = ∞ ** TCTL CTL + Formula clocks, definito su TTS. D = set formula clocks | ϕ ::= p | ¬(ϕ) | ϕ∨ϕ | E[ϕUϕ] | A[ϕUϕ] | α∈Cstr(C∪D) | z in ϕ - z in ϕ, z∈D: freeze indentifier: | z in ϕ is valid in state s if ϕ holds in s where clock z start from 0 Esempi: | E (ϕ $U^{\le{n}}$ ψ) = reset z in E (ϕ U (z≤n ∧ ψ)) | $AF^{=n}(\phi)$ = reset z in AF(z = n ∧ ϕ) *** TCTL secondo induzione strutturale 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) * Equivalenze trace: stesso sequenza di azioni 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': q\underrightarrow{a}$q' ∧ p' ~ q') - Bisimulazione: ∀p,q⊆P×P p≈q iff ∀a: p $\underrightarrow{a}$ p' → ∃q': q $\underrightarrow{a}$ q' and ∀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. - Strong Fairness: GF(enᵢ) → GF(exᵢ) un processo abilitato infinite volte puo` essere eseguito infinite volte. - Weak Fairness: FG(enᵢ) → GF(exᵢ) un processo che da un punto in avanti e` sempre abilitato puo` essere eseguito infinite volte 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) ≠ ∅