FSV Kapitel 2

Descripción

2 Invarianten-Verifikation und Erreichbarkeitsanalyse
Stael Tchinda
Fichas por Stael Tchinda, actualizado hace más de 1 año
Stael Tchinda
Creado por Stael Tchinda hace casi 5 años
25
0

Resumen del Recurso

Pregunta Respuesta
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
Mostrar resumen completo Ocultar resumen completo

Similar

FSV Kapitel 7
Stael Tchinda
Mesopotamia y Egipto
irinavalin
Advanced English II
cristinaruizald
Disoluciones
Victor Rodriguez
La acentuación de diptongos, triptongos e hiatos
Elisa Tormo Guevara
Compás de 4/4
mariajesus camino
ARTE DE GRECIA
Alex Velazquez
COMUNICACIÓN EN INTERNET
Custodio García
Todos mis RECURSOS...
Ulises Yo
Historia de la Literatura
katya Ceballos
MICROECONOMÍA
ingrinati