427 lines
16 KiB
Org Mode
427 lines
16 KiB
Org Mode
* 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\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, ∑, 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: σʲ ⊧ φ ∧ σⁱ ⊧ ψ
|
||
# | σⁱ ⊧ φ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 = <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:
|
||
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, ∑, Δ, 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) ≠ ∅
|