2020-06-10 12:46:44 +02:00
|
|
|
|
Rete di petri: grafo bipartito, Sistema: stato composito
|
|
|
|
|
|
Rete colorata: cd: P∪T → C, Post[p,t]: cd(t) → bag(cd(p))
|
|
|
|
|
|
| Transition system: <V, ∑, T, ∑₀, R (→)>
|
|
|
|
|
|
* Semantiche:
|
|
|
|
|
|
** Peled: (Induzione Strutturale)
|
|
|
|
|
|
σⁱ il suffisso sᵢ, sᵢ₊₁, ... (σ⁰ = σ)
|
|
|
|
|
|
| σⁱ ⊧ p, p is proposition if sᵢ ⊧ p
|
|
|
|
|
|
** Katoen:
|
|
|
|
|
|
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)
|
|
|
|
|
|
** Katoen CTL:
|
|
|
|
|
|
| Pₘ(s) = {σ ∈ Sʷ| σ₀ = s} σ path - sequenza di s
|
|
|
|
|
|
Per induzione strutturale su ϕ:
|
|
|
|
|
|
| M,s ⊧ p iff p∈L(S)
|
|
|
|
|
|
| M,s ⊧ ¬φ iff ¬(M,s ⊧ φ)
|
2020-06-10 16:36:17 +02:00
|
|
|
|
** Operatori derivati
|
|
|
|
|
|
- EGφ = ¬AF¬φ
|
|
|
|
|
|
- AXφ = ¬EX¬φ
|
2020-06-10 12:46:44 +02:00
|
|
|
|
** TCTL
|
|
|
|
|
|
CTL + Formula clocks, definito su TTS.
|
|
|
|
|
|
D = set formula clocks
|
|
|
|
|
|
| ϕ ::= p | ¬(ϕ) | ϕ∨ϕ | E[ϕUϕ] | A[ϕUϕ] | α∈Cstr(C∪D) | z in ϕ
|
|
|
|
|
|
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)
|
|
|
|
|
|
** 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) ≠ ∅
|
