Modallogik Flashcards
(9 cards)
Definition 5.2: Transitionssystem (oder Kripkestruktur) (Skript 122)
Ein Transitionssystem oder eine Kripkestruktur mit Aktionen aus A und atomaren Eigenschaften {P_i : i element I} ist eine Struktur:
K = (V, (E_a) a element A, (P_i) i element I)
mit Universum V (dessen Elemente Zustände oder Welten genannt werden), zweistelligen Relationen E_a teilmenge V x V (a element A ) (Welche Transitionen zwischen Zuständen beschreiben) und einstelligen Relationen (Eigenschaften der Zustände) P_i teilmenge V (i element I). Statt (u, v) element E_a schreiben wir oft auch u —-a—-> v.
Wie sind Diamond und Box definiert?
Diamond: K,v |= <a>psi, wenn ein w existiert mit (v, w) element E_a und K,w |= psi.</a>
Box:
Box: K,v |= [a]psi, wenn für alle w mit (v, w) element E_a gilt, dass K,w |= psi.
</a>
Satz 5.6 Zusammenhang FO^2 (zwei-Variablen-Fragment von FO) und ML (Skript 124)
Zu jeder Formel psi element ML gibt es eine Formel psi*(x) elemenet FO^2, so dass für alle Transitionssysteme K und alle Zustände v von K gilt:
K,v |= psi gdw K |= psi*(v)
Definition 5.8: Bisimulation (Skript 125)
Eine Bisimulation zwischen zwei Transitionssystemen K = (V, (E_a) a element A, (P_i) i element I) und K’ = (V’, (E’_a) a element A, (P’_i) i element I) ist eine Relation Z teilmenge V x V’, so dass für alle (v, v’) element Z gilt:
1) v element P_i gdw. v’element P’_i für alle i element I
2) Hin: Für alle a element A, w element V mit v –a–> w existiert ein w’ element V’ mit v’ –a–> w’ und es ist (w, w’) element Z
Her: Für alle a element A, w’ element V’ mit v’ –a–> w’ existiert ein w element V mit v –a–> w und es ist (w, w’) element Z
Wann gewinnt Spieler II ( dieser Spieler antwortet immer auf Züge von Spieler I)? (Skript 125)
Was bedeutet es, wenn Spieler II innerhalb von n Zügen gewinnt?
Spieler II gewinnt genau dann das Bisimulationsspiel auf K, K’ von (u, u’), wenn K,u ~ K’,u’ (also wenn (K,u) und (K’,u’) bisimilar sind).
Es gilt für alle n element Nat.Z., dass II genau dann das n-Züge-Bisimulationsspiel von (v, v’) aus gewinnt, wenn K,v ~_n K’,v’
Definition 5.13 Modaltiefe (Skript 127)
Die Modaltiefe einer Formel psi element ML ist induktiv definiert durch:
1) md(psi) = 0 für aussagenlogische Formeln psi
2) md(nicht psi) = md(psi)
3) md(psi * phi) = max ( md(psi), md(phi) ) für * bel. junktor
4) md(<a>psi) = md([a]psi) = md(psi) + 1</a>
Satz 5.15 Zusammenhang logische Äquivalenz, bisimilar (bzw. n-bisimilar) (Skript 128)
Für Kripkestrukturen K, K’ und u element K,u’ element K’ gilt:
1) Aus K,u ~ K’, u’ folgt K,u log. äquivalent_ML K’, u’
2) Aus K,u ~_n K’, u’ folgt K,u log. äquivalent^n_ML K’, u’
(logisch äquivalent ist ein gleichzeichen mit 3 strichen, die logische Äquivalenz^n bedeutet, dass ML Formeln der Tiefe 3 oder kleiner keinen Unterschied zwischen den Strukturen feststellen können)
Was ist ein endlich verzweigtes Transitionssystem?
Welcher Zusammenhang ergibt sich bezüglich bisimilarität und logischer äquivalenz? (Skript 129)
Ein Transitionssystem ist endlich verzweigt, wenn für alle Zustände v und alle Aktionen a die Menge vE_a := {w: (v,w) element E_a} der a-Nachfolger von v endlich ist. Insbesondere ist natürlich jedes endliche Transitionssystem endlich verzweigt.
Seine K, K’endlich verzweigte Transitionssysteme. Dann gilt K,u ~ K’,u’ genau dann, wenn K,u log. äquivalent_ML K’,u’
Wann ist ein Transitionssystem ein Baum? Was ist die Baummodell-Eigenschaft? (Skript 130)
Ein Transitionssystem K = (V, (E_a) a element A, (P_i) i element I) mit einem ausgezeichneten Knoten w ist ein Baum, wenn:
1) E_a SCHNITT E_b = leere Menge für alle Aktionen a != b
2) für E = VEREINIGUNG a element A (E_a) der Graph (V, E) ein gerichteter Baum mit Wurzel w im Sinn der Graphentheorie ist.
Zur Baummodell-Eigenschaft:
Die Abwicklung von Transitionssystem K wird so gebildet, dass jeder Pfad in K als eigenes Objekt angesehen wird (Kreise sind unendliche Pfade) und so an einen betrachteten Zustand v angehangen wird, dass die Pfade die gleichen wie vorher sind. Die Abwicklung von K vom Zustand v aus ist bisimilar zu K selbst:
K,v ~ T_(K,v) , v
Die Baummodell-Eigenschaft besagt nun, dass jedes Modell in einen Baum abgewickelt werden kann, der auch Modell ist.
Satz 5.21: ML hat die Baummodell-Eigenschaft
