* Simboli:
- sqcap: ⊓
- box: □
- a\b: a̱
- Vert: ‖
- $\underrightarrow{a}$ (toggle latex fragment): $\underrightarrow{a}$
- varphi: φ
- models: ⊧

* 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 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: ∀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.
** 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 | 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ʲ ⊧ φ ∧ Rⁱ ⊧ ψ