After Test Thread 29.06.2012

[DMexx]

Na das war ja mal eine lustige Prüfung

Prof. Veith hat am Montag noch ausgeschickt dass er die fehlenden Unterlagen nicht mehr hochladen wird und zur Prüfung nur alecture1 - alecture5 kommt.
2 Tage vor der Prüfung übrigens noch die Überraschung (für mich zumindest) dass beliebige Unterlagen erlaubt sind.

Beispiel 1.
War dann jedenfalls zu dem Stoff der nicht in den verfügbaren Unterlagen war

Neues Sprachelement: Tp. Ist ähnlich wie Fp, aber nur für gerade States am Pfad, also p v xxp v xxxxp usw
Dafür sollte für Bounded Modelchecking eine Formel/Algorithmus angegeben analog zu denen für andere Operation die bekannt sind.
Wie gesagt, die Bounded Modelchecking Unterlagen wurden nicht hochgeladen.
Gott sei dank war Prof. Veith kooperativ und hat die Angabe einfach umgeändert auf Symbolic Modelchecking, es soll also
Es war also im Prinzip die Prozedur Check(ETp) anzugeben.

Beispiel 2.
Selbes Sprachkonstrukt T, einen Algorithmus angeben der (direkt auf einer Kripkestructure) T mit einem Set an Fairness-Constraint prüft

Beispiel 3.
Mehrere Angaben in Sätzen, dazu war eine entsprchende CTL* Formel anzugeben. Gegeben eine Kripkestructure, deren Initial State s0 Label i hat und AP = {a,b,c,d,i} (welche APs bin ich ma nimma ganz sicher, vl mehr oder weniger, is auch ned so wichtig)
a) vom Initial State s0 ist ein State reachable, in dem "a" gilt
b) Es gibt einen Loop in dem "a" und "b" vorkommen
c) auf allen Pfaden beginnend im Initial State s0 tritt ein "a" auf
d) Der Initial State befindet sich in einem Loop
e) Die Kripke Structure ist deterministisch, also jeder Nachfolgezustand ist eindeutig anhand seiner Labels identifizierbar


Beispiel 4.
Mehrere Aussagen die als wahr/falsch zu kennzeichnen waren

a) CTL ist ein Subset von LTL
b) LTL ist ein Subset von CTL*
c) Jede CTL Formel kann auch als durch eine equivalente Formel mit nur E und ohne A angegeben werden (oder wars andersrum?)
d) Jede LTL Formel kann auch durch eine negationsnormalform mit nur E und ohne A angegeben werden (bin mir nicht mehr sicher ob die Aussage wirklich genau so war, vl wars auch ohne negation?)
e) kA
f) kA
g) kA
i) Eine SMV Spezifikation ist als BDD gegeben
j) In SMV ist jedem State in der Kripke Struktur ein BDD zugeordnet


Jedes Beispiel 20 Punkte Wert, Übungszettel wurden einfach mit abgegeben, ich würde mal vermuten dass die Übung auch 20 Punkte wert ist und dann einfach aus den resultierenden max 100 Punkten die Note genommen wird...