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 alrededor de 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
Apuntes para Aprender Inglés
maya velasquez
CIENCIAS AUXILIARES DE QUÍMICA ORGÁNICA
Luis Carrillo
Ingeniería Industrial
monicasorelly14
Autores y obras de las generación del 98
maya velasquez
MODELOS PEDAGÓGICOS
wfas197
Web 2.0 and other emerging technologies applied to research
patricia sarria
Guía para Tener Éxito en los Exámenes
Diego Santos
¿COMO HACER UN CUADRO SINOPTICO?
luisa valentina castaño acuña
CONCEPTOS BÁSICOS DE INTELIGENCIA
Edgar Sarzosa
Tejidos animales
Enrique Bravo