| gerichtete Graphen mit Knotenbeschriftung |
     |
Meine Frage:
Wir betrachten Transitionssysteme über der Signatur {E,P,Q} für ein zweistelliges Relationssymbol E und einstellige Relationssymbole P und Q, also gerichtete Graphen mit Knotenbeschriftung.
a)Geben Sie eine FO-Formel an, die definiert, dass jeder Knoten, der einen Nachfolger hat, auch einen Nachfolger in Q hat.
b)Beweisen oder widerlegen Sie mithilfe des Model Checking Spiels, dass Ihre Formel im unten angegebenen Graphen mit Universum {v,v'}
gilt. Konstruieren Sie dazu den Spielgraphen und geben Sie eine Gewinnstrategie für die Verifiziererin oder den Falsifizierer an.
Meine Ideen:
Hallo,
ich besuche zurzeit die Vorlesung Mathematische Logik und muss die obere Aufgabe lösen. Leider habe ich Probleme bei der FO-Formelaufstellung. Könnt ihr mir helfen, sodass ich die b) selbständig bearbeiten kann?
Liebe Grüße Anjuta
Anjuta hat dieses Bild (verkleinerte Version) angehängt:
|
