Erstellt von Stael Tchinda
vor mehr als 5 Jahre
|
||
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 |
Möchten Sie mit GoConqr kostenlos Ihre eigenen Karteikarten erstellen? Mehr erfahren.