FB18 - Das Forum für Informatik

fb18.de / Diplom Informatik / Theoretische Informatik (HS)

(PNL) Fragen Faire Kripke-Struktur (and more)

(PNL) Fragen Faire Kripke-Struktur (and more) 2009-06-28 16:38
Anonymer User
hi @all,

Bei der Defintion 5.48 - Faire Kripke-Struktur (S.212 / Modellierung und Analyse Teil 2 / WiSe 2006/2007)

bin ich mir nicht sicher was denn wirklich

[Latex] inf$( \pi ) = \{s|s=s_i fuer undendlich viele i \in N_0 \} $[/Latex]

heißt/ bedeutet.

gruß notME

RE: (PNL) Fragen Faire Kripke-Struktur (and more) 2009-07-05 14:57
Anonymer User
Hi…

\pi ist ein Pfad bestehend aus einer (unendlichen) Folge von Zuständen der Kripkestruktur, also
\pi = s_0 s_1 s_2 ….
Dabei sind s_0, s_1, s_2 nicht die Bezeichnung der Zustände in der Kripkestruktur, sondern eben einfach die Zustände in dem Pfad. Wenn du z.B. in der Kripkestruktur S = {a,b,c} hast, dann kann in dem Pfad jetzt auch nur a, b und c auftreten (z.B. \pi = abbcabbbbb…). Schreib ich dann \pi = s_0 s_1 s_2 …., dann ist im Beispiel also s_0 = a, s_1 = b, s_2 = b usw. Die Indizierung bei \pi = s_0 s_1 …. ist also dafür da vom so-und-so-vielten (vom i-ten) Zustand im Pfad sprechen zu können.

\inf(\pi) ist nun gerade die Menge all jener Zustände, die unendlich oft in \pi auftreten, d.h. all jener Zustände, nennen wir sie mal s, für die s gerade einem Zustand s_i in dem Pfad \pi entspricht und das unendlich oft, d.h. es ist z.B. s = s_3 und s = s_6 und s = s_8 und …. sprich: es gibt unendlich viele Indizes i derart, dass s_i gerade gleich s ist (wobei s dann wieder ein Zustand der Kripkestruktur ist).

Über \inf(\pi) wird dann die Fairness der Kripkestruktur definiert.

Im neuen Skript ist diese Definition übrigens etwas anders (sagt aber im Endeffekt das gleiche aus).

Hoffe es hilft!
Frank :)