16 KiB
Executable file
- Simboli:
- 1.1 Petri Nets
- 1.2 Reti di Petri colorate
- 1.3 Tecniche Strutturali
- 2.1 Algebra dei Processi
- 3.1 Linear Temporal Logic
- 3.2 Computational Tree Logic
- CTL*
- 4.1 Time
- Equivalenze
- Fairness
- Automa di Buchi
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, T, →, W> |
- 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 = <P, T, Pre, Post> |
-
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 = <N, m₀> |
| 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 = <P, T, Pre, Post, C, cd> |
- 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 <t,c> 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§ $\underrightarrow{\mu}$ E'§
E $\underrightarrow{\mu}$ E' —————————–(μ ∈ S) E§ $\underrightarrow{\tau}$ E'§
3.1 Linear Temporal Logic
Transition System
| TS = <V, ∑, T, I, R> |
- 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: σʲ ⊧ φ ∧ σⁱ ⊧ ψ |
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 = <Loc, E, L₀, Label, C, Reset, Guard, Inv> |
- 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 = <L, v> |
| reset(x in y)(y) = v(y) if y ≠ x else 0 |
| v ⊧ x≤c iff v(x)≤c |
| v ⊧ x<c iff v(x)<c |
| v ⊧ ¬α iff v¬⊧α |
| v ⊧ α∧β iff v⊧α ∧ v⊧β |
Timed Transition System
| M(A) = <S, s₀, →> |
- S = {(l, v) ∈ L×V(C) | v⊧inv(l)}
- s₀ = (l₀, v₀), v₀(x) = 0 ∀x
-
→ ⊆ S × R∪{*} × S:
-
(l,v)$\underrightarrow{*}$(l', (reset Reset(edge) in v)):
- edge ∈ E
- v⊧guard(edge)
- (reset Reset(edge) in v)⊧inv(l')
-
(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_rightarrow{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, ∑, Δ, F>
- 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) ≠ ∅