diff --git a/anno3/vpc/CTLonPetriNets-1.pdf b/anno3/vpc/CTLonPetriNets-1.pdf
new file mode 100644
index 0000000..9c23b47
Binary files /dev/null and b/anno3/vpc/CTLonPetriNets-1.pdf differ
diff --git a/anno3/vpc/altro/20-temporal.pdf b/anno3/vpc/altro/20-temporal.pdf
new file mode 100644
index 0000000..2890087
Binary files /dev/null and b/anno3/vpc/altro/20-temporal.pdf differ
diff --git a/anno3/vpc/consegne/3/analisi.org b/anno3/vpc/consegne/3/analisi.org
new file mode 100644
index 0000000..883c480
--- /dev/null
+++ b/anno3/vpc/consegne/3/analisi.org
@@ -0,0 +1,24 @@
+* Proprieta` del modello
+
+Ogni modello successivamente mostrato rispetta le seguenti proprieta`:
+1. Mutua esclusione (safety): garantisce che al piu` un solo processo e` nella
+   sezione critica ad ogni istante
+   | G (¬cₚ∨¬c_{q}) 
+2. Assenza di deadlock (liveness): ogni qualvolta un processo e` in
+   attesa di entrare nella sezione critica, eventualmente verra`
+   concesso ad un processo di entrare nella sezione critica
+   | G(wₚ → F(cₚ∨c_{q})
+3. Assenza di starvation individuale (strong fairness): ogni qualvolta un processo e` in
+   attesa di entrare nella sezione critica, eventualmente gli verra` concesso
+   | GFcₚ
+Possiamo convertire queste tre formule LTL in formule equivalenti CTL
+anteponendo l'operatore di stato A:
+   | AG (¬cₚ∨¬c_{q}) 
+   | AG(wₚ → AF(cₚ∨c_{q})
+   | AGAFcₚ
+Benche` non tutte le formule LTL possono essere convertite in una
+formula CTL equivalente anteponendo ad ogni operatore temporale
+l'operatore di stato A, per queste tre proprieta` possiamo
+ 
+[ ] Correggi LTL E CTL dell'ultima.
+[ ] Chiedi a galla` se e` giusto in termini di liveness safety e fairness