FSV Kapitel 2

Description

2 Invarianten-Verifikation und Erreichbarkeitsanalyse
Stael Tchinda
Flashcards by Stael Tchinda, updated more than 1 year ago
Stael Tchinda
Created by Stael Tchinda about 5 years ago
25
0

Resource summary

Question Answer
Blatt 2 Ready ? Go !
Aus welchen Komponenten besteht ein Transitionssystem T ? - Menge Q aller Zustände - Teilmenge (σ hoch I) c Q der Startzustände (nicht leer) - Transitionsrelation -> c Q × Q
Was ist eine Spur? endliche Folge von s = s_0, s_1, . . . , s_n von Zuständen s_i € Q, so dass für alle o<= i < n: s_i -> s_(i+1) UND s_0 € (σ hoch I)
Was ist eine Region? Teilmenge σ c Q von Zuständen
Welche Beispiele für Regionen kennen Sie aus der Vorlesung? - Startzustände (σ hoch I) , - alle erreichbaren Zustände (σ hoch R), - Nachfolgerzustand post(s) eines Zustands s
Wie skaliert die Laufzeit der aufzählenden Suche? linear in der Anzahl von erreichbaren Transitionen
Wann terminiert die aufzählende Suche? Wenn erreichbare Region endlich ist
Wofür ist die aufzählende Suche eigentlich gut? - Einfach zu implementieren - Liefert alle erreichbaren (konkreten) Zustände - Kann zur Verifikation benutzt werden - Für kleine, endliche Systeme ausreichend - Für größere Systeme existieren bessere Verfahren (dazu kommt noch ein Blatt) - Generelle Struktur ders Algorithmus (Suche mit Warteliste) bleibt gleich
2.1 Eigenschaften von Transitionssystemen T hoch R Ready for the rest ? Go !
Was sind diese (4) Eigenschaften ? 1. endlich: Q ist endlich 2. endlich verzweigend: für alle s : post(s) ist endlich 3. endlich erreichbar: Es gibt n >= 0, so dass alle erreichbaren Zustände von T in <= n Transitionen erreichbar sind 4. Reflexivität: Für alle s € Q : s -> s
Was ist der Branching-Faktor k von T ? Das Maximum der - Anzahl von Startzuständen, - max. Anzahl von Nachfolgern, und - max. Anzahl von Vorgänger
Was ist der Durchmesser n von T ? Die maximale Entfernung vom Startzustand
Was ist die maximale Anzahl von Zustände? k hoch n
2.2 Erreichbarkeitsproblem Ready for the rest ? Go !
Was ist das Algorithmus für die Aufzählennde Suche ? Input : T = (Q, (σ hoch I) ,->) Output: erreichbare Region (σ hoch R) von T Local : Menge τ von Zuständen von Q 1 begin 2 (σ hoch R) := ∅; 3 τ := (σ hoch I) ; 4 while τ != ∅; do 5 wähle s € τ ; τ := τ \ {s}; 6 if s /2 !€ (σ hoch R) then 7 (σ hoch R) := (σ hoch R) UNION {s}; 8 τ := τ UNION post(s); 9 end 10 end 11 end
Was ist das Algorithmus für die symbolische Suche ? Input : T = (Q,σ hoch I,→) Transitionssystem Input : σ hoch T Zielregion Output: Antwort zum Erreichbarkeitsproblem (T, σ hoch T) Local : Erreichbare Region σ hoch R von T Local : Menge τ von Zuständen von Q 1 begin 2 σ hoch R := ∅; 3 τ := InitReg(T) // d.h. σ hoch I; 4 while true do 5 if (σ hoch R)∩(σ hoch T) != ∅ then return YES; 6 if τ ⊆ σ hoch R then return NO; 7 σ hoch R := σ hoch R∪τ; 8 τ := PostReg(τ, T) 9 end 10 end
Show full summary Hide full summary

Similar

FSV Kapitel 7
Stael Tchinda
Spanish Vocabulary- Intermediate
PatrickNoonan
AS Unit 2 Physics Flashcard Deck
Callum McClintock
OCR AS Biology - Enzymes
Chris Osmundse
GCSE French Edexcel High Frequency Verbs: First Set
alecmorley2013
Of Mice and Men
becky_e
History - Germany 1918 - 1945
Grace Evans
Edexcel Additional Science Biology Topic 1- Genes and Enzymes
hchen8nrd
Chemistry 1
Peter Hoskins
exothermic and endothermic reactions
janey.efen
Macbeth Quotes To Learn
Sophie Brokenshire