1.8 KiB
1.8 KiB
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 ⊧ φ) |
Operatori derivati
- EGφ = ¬AF¬φ
- AXφ = ¬EX¬φ
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) ≠ ∅