diff --git a/anno3/vpc/3.logica/extra.07.utexas.pdf b/anno3/vpc/3.logica/extra.07.utexas.pdf
new file mode 100644
index 0000000..1f36c8d
Binary files /dev/null and b/anno3/vpc/3.logica/extra.07.utexas.pdf differ
diff --git a/todo.org b/todo.org
index 96a3d31..b697f43 100644
--- a/todo.org
+++ b/todo.org
@@ -1,4 +1,4 @@
-* TODO VPC [21/22]
+* TODO VPC [21/23]
 - [X] Controlla good latex
 - [X] Uppaal muovi cartella file
 - [X] Rimuovi "Contents" da ogni .org
@@ -12,7 +12,8 @@
 - [X] spiega nelle relazioni che bounded se RS finito
 - [X] spiega nelle relazioni che bounded quando coperta da p-semiflows
 - [X] Vedi bisimulazione ed equivalenze in teoria analisi
-- [ ] Teoria [0/8]
+- [ ] Che significa urgente in uppaal?
+- [-] Teoria [1/13]
   - [ ] Hierarchy of equivalences
   - [ ] algebra.extra.lucca: internal/external choices
   - [ ] Observer e testing equivalence
@@ -21,6 +22,11 @@
   - [ ] Vedi da relazioni procedure dimostrazione deadlock
   - [ ] Impara equivalenze come le spiega lei
   - [ ] Formalizza algoritmo bisimulazione
+  - [ ] Vedi slide 42 ltl: liveness, safety, fairness, anche in CTL
+  - [ ] CTL e LTL: set operatori minimo per derivare altri
+  - [X] Manca CTL* ?
+  - [ ] Pstate?
+  - [ ] BDD e decision diagrams, tutto Amparore
 - [X] rete A, b, c, d [6/6]
   - [X] Spiega p-t-semiflows analysis: deadlock e liveness, boundness
   - [X] sulle slide, quando si chiede come deve  decidere il master