# Blatt 4
Lukas Bruns
Robin Faeseke
Aufgabe 1


Aufgabe 2
1. χχχa
2. χχ¬Ga
3. b R(a ∧ b)
4. true
5. a ∧ Fb
6. false
7. a ∧ (χbUc)
8. (Fa)χ(Fa) -> ¬Ga

Aufgabe 3
1. Gilt nicht, da erster Zustand b ist.
2. Gilt nicht, da der nächste Schritt zu a sein könnte.
3. Gilt, da auf dem komplett Pfad irgendwann mal a gilt (z.B. unten links oder in der Endlosschleife).
4. Gilt, da wir von Start aus in allen möglichen Läufen ein a treffen bevor wir auf ein c treffen.
5. Ist erfüllt, da wir irgendwann in unserem Transitionssystem in die Endlosschleife kommen und in dieser auf dem komplett nachfolgendem Pfad a gilt.
6. Gilt nicht, da der Term (G(¬c->Xb)) immer erfüllt sein muss. Dies ist aber für den Fall c ist erfüllt und wir wählen danach a nicht gegeben.
7. Gilt nicht, da wir in dem nächsten Schritt nicht von c zu b kommen.
8. Gilt, da G(true) immer gilt und wir eine oder Verknüpfung haben und somit Xb irrelevant wird.