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
English Vocabulary
Niat Habtemariam
IB SL Biology: Cells
mcgowan-w-10
A2 Ethics - Virtue Ethics
Heloise Tudor
Biology B1
Phoebe Drew
Geography - Case Studies
jacobhatcher97
Computer Systems
lisawinkler10
Whole Number Glossary L1
Lee Holness
AN ECONOMIC OVERVIEW OF IRELAND AND THE WORLD 2015/16
John O'Driscoll
General questions on photosynthesis
Fatima K
1_PSBD New Edition
Ps Test