bparodi/UniTO
1
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
UniTO/anno3/vpc/orale/preparazione.org
Benedetta Parodi c2122d9568 resurrect
2024-10-29 09:11:05 +01:00

16 KiB
Executable file
Raw Permalink Blame History

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:

    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_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) ≠ ∅