Thomas und die Modallogik

| Back to Overview

Grundlagen

Die Modallogik handelt von Transitionssystemen/Graphen.

Definition:

  • Alle aussagenlogischen Formeln mit Aussagenvars. PiP_i sind in ML.
  • Wenn φ,ψ∈ML\varphi, \psi \in ML dann auch ¬ψ,(φ∨ψ),...\lnot \psi, (\varphi \lor \psi), ...
  • Wenn φ∈ML\varphi \in ML und a∈Aa \in A (das heißt die aa ist in den Aktionen wie im Diagramm), dann gehört auch ⟨a⟩φ,[a]φ\langle a \rangle \varphi, [a]\varphi zu ML.
  • Falls nur eine Aktion vorhanden ist ∣A∣=1|A| = 1 dann wird auch ⋄φ\diamond \varphi (möglicherweise φ\varphi) und □φ\square \varphi (notwendigerweise φ\varphi)

Die Struktur der Modallogik ist die Kripkestruktur mit Aktionen AA. K=(V,(Ea)a∈A,(Pi)i∈I)K = (V, (E_a)_{a \in A}, (P_i)_{i \in I}). Die Knoten sind natürlich das Universum.

Die Modellbeziehung: K,v⊨φK,v \models \varphi (d.h. φ\varphi gilt im Zustand vv von KK).

∃\exists ist verglichbar mit dem ⋄\diamond und analog □\square.

Es ist leicht einzusehen, dass für jede Formel φ∈ML\varphi \in ML ein Formel φ∗(x)∈FO2\varphi*(x) \in FO^2 gibt. Hierbei ist FO2FO^2 alle FO-Formeln mit nur zwei Variablen x,yx,y.

Bisimulation

Das wichtigste bei der Modallogik ist die Bisimulation. Hier werden wie bei EF-Spielen die Ununterscheidbarkeit von zwei Kripkestruktur nachgewiesen.

Eine Bisimulation zwischen K,K′K, K' ist eine Relation Z⊆V×V′Z \subseteq V \times V', sodass für alle (v,v′)∈Z(v,v') \in Z gilt:

  • v∈Piv \in P_i gdw. v′∈Pi′v' \in P'_i für alle i∈Ii \in I
  • Hin: Für alle a∈A,w∈Va \in A, w \in V mit v→awv \overset{a}{\to}w existiert ein w′∈V′w' \in V' mit v′→aw′v' \overset{a}{\to}w' und es ist (w,w′)∈Z(w,w') \in Z
  • Her: Genau anderherum für alle a∈A,w′∈V′a \in A, w' \in V' ...

Zwei Strukturen sind bisimilar K,u∼K′,u′K,u \sim K', u' wenn es eine Bisimulation gibt.

Das Bisimulationsspiel geht dann wie folgt:

Start bei den Knoten (u,u′)(u,u') bzw. den Gegebenenstartknoten

Eigentlich genau wie bei den EF-Spielen, nur das man nur anhand den Vorgegeben Transitionen arbeiten kann und keinen Knoten zweimal besuchen kann. Falls man nichtmehr weiter ziehen kann ists für dich vorbei.

Es geht dann wieder um Gewinnstrategien. Spiele II gewinnt das Bisimulationsspiel von u,u′u,u' wenn es eine Bisimulation von u,u′u,u' gibt.

Genau das gleiche gilt für das n-Züge-Bisimulationsspiel (K,v∼nK′,v′K, v \sim_n K', v')

Die Modaltiefe ist das gleiche wie der Quantorenrang qrqr.

Elementare Äquivalenz und m-Äquivalenz ist gleich wie bei Prädikatenlogik. Notiert: K,v≡MLK′,v′K,v \equiv_{ML} K',v' und K,v≡MLnK′,v′K,v \equiv_{ML}^n K',v'

Sind K,K′K,K' endlich verzweigte (d.h. alle Zustände haben nur endlich viele Nachfolger) Transitionssysteme, dann gilt K,v∼K′,v′K,v \sim K', v' genau wenn K,v≡MLK′,v′K,v \equiv_{ML} K',v' gilt.

Erfüllbar φ∈ML\varphi \in ML haben immer ein Baummodell, also ein Modell welches ein Baum ist.

Temporale Logiken

k.p. mach ich erstmal nicht.

< Zur sibd Website
Zur cesti Website >