FSV Kapitel 2

Beschreibung

2 Invarianten-Verifikation und Erreichbarkeitsanalyse
Stael Tchinda
Karteikarten von Stael Tchinda, aktualisiert more than 1 year ago
Stael Tchinda
Erstellt von Stael Tchinda vor mehr als 5 Jahre
26
0

Zusammenfassung der Ressource

Frage Antworten
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
Zusammenfassung anzeigen Zusammenfassung ausblenden

ähnlicher Inhalt

FSV Kapitel 7
Stael Tchinda
Geographie Quiz
AntonS
Vererbung
Greta Warnke
Einführung in die Forschungsmethoden Kapitel 1
Angelina Idt
Vektorendefinition
Sinan 2000
Euro-FH // Zusammenfassung PEPS3
Robert Paul
PR 2018/19 GESKO VO 1-6
Adrienne Tschaudi
Vetie Tierseuchen 2018
Schmolli Schmoll
Basiswissen_MS-4.2_Foliensatz I_Stand_03.11.19
Bernd Leisen
MS-1.3 Folienpaket 4
Lukas Imwalle
Vetie Innere Medizin 2020
Ferdinand Kähn