From a18e6f6cce07081c33042be6660e0dea58f19c51 Mon Sep 17 00:00:00 2001
From: Francesco Mecca <me@francescomecca.eu>
Date: Mon, 8 Jun 2020 18:06:52 +0200
Subject: [PATCH] ltl

---
 ...640f875a08c76d95b581f56e3ad36bf4897eb7.png | Bin 0 -> 180 bytes
 ...3cad1b57df0737d759930f43f9bb823b14f9a1.png | Bin 0 -> 187 bytes
 anno3/vpc/orale/preparazione.org              |  40 ++++++++++++++++++
 3 files changed, 40 insertions(+)
 create mode 100644 anno3/vpc/orale/ltximg/org-ltximg_2f640f875a08c76d95b581f56e3ad36bf4897eb7.png
 create mode 100644 anno3/vpc/orale/ltximg/org-ltximg_903cad1b57df0737d759930f43f9bb823b14f9a1.png

diff --git a/anno3/vpc/orale/ltximg/org-ltximg_2f640f875a08c76d95b581f56e3ad36bf4897eb7.png b/anno3/vpc/orale/ltximg/org-ltximg_2f640f875a08c76d95b581f56e3ad36bf4897eb7.png
new file mode 100644
index 0000000000000000000000000000000000000000..8affc13b4d0be18e656f3f245ff05b9215beeba0
GIT binary patch
literal 180
zcmeAS@N?(olHy`uVBq!ia0vp^96-#&!VDzWZg{v3NGS&Rgt!9f*Y7^t**p6B1<1=Q
z=;`Ul#V6L*H}UcD@7aI2r*9&EgoZXy5odu%WHAE+-w_aIoT|+y4HUHWba4#fkWEfV
zNJwH}N)vd<bR;pAlP8Ch?Ih1!9=2yZQ969x5_@JuiW?X#mu5~qcq*!qhmDnujp0x`
W+cLFXZJU9HFnGH9xvX<aXaWFjbuWAX

literal 0
HcmV?d00001

diff --git a/anno3/vpc/orale/ltximg/org-ltximg_903cad1b57df0737d759930f43f9bb823b14f9a1.png b/anno3/vpc/orale/ltximg/org-ltximg_903cad1b57df0737d759930f43f9bb823b14f9a1.png
new file mode 100644
index 0000000000000000000000000000000000000000..357f39552aa52d9bd636d16ce058e4f1c521dc1c
GIT binary patch
literal 187
zcmeAS@N?(olHy`uVBq!ia0vp^oFL4?3?zm2ODh8@g8-ipS0MfR-Df>L{kZtVJNF;Y
zoxg~WkN@<!OY-sxJ$)1H>>Yjm0&?>TYU`W!>_5C_-A2JjT-!kg6?jAzGcfQS0b$0e
z+I-SLK|@a$#}E$L<b;4S(*z*UW)qUxyz0D>!3K>zkL(XDnDL?OJM)yYf-FMm4^}V=
aC46PDbLGBMb<F_e8U{~SKbLh*2~7Z=96Kif

literal 0
HcmV?d00001

diff --git a/anno3/vpc/orale/preparazione.org b/anno3/vpc/orale/preparazione.org
index e526060..17f36d3 100644
--- a/anno3/vpc/orale/preparazione.org
+++ b/anno3/vpc/orale/preparazione.org
@@ -4,6 +4,8 @@
 - a\b: a̱
 - Vert: ‖
 - $\underrightarrow{a}$ (toggle latex fragment): $\underrightarrow{a}$
+- varphi: φ
+- models: ⊧
 
 * 1.1 Petri Nets
 ** Definizione
@@ -220,3 +222,41 @@ 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ⁱ ⊧ ψ