Bestimmung: Kripke-Struktur < Formale Sprachen < Theoretische Inform. < Hochschule < Informatik < Vorhilfe
|
| Status: |
(Frage) überfällig  | | Datum: | 17:06 Fr 04.12.2009 | | Autor: | Wilson |
| Aufgabe | | Geben Sie eine Kripke-Struktur K, s an, so dass K, s |= AFG p, aber K, Not |= AFAG p. |
Hallo zusammen,
die Aufgabe ist aus dem Bereich Model Checking. Hoffe, dass das hier hingehört.
Im Prinzip geht es darum beispielhaft zu zeigen, dass AFG nicht gleich AFAG ist. AFG kann nur in LTL und AFAG in CTL dargestellt werden. Vermutlich habe ich LTL noch nicht richtig verstanden. Kann mir jemand erklären, was AFAG und AFG voneinander unterscheidet?
Ich danke im Voraus!!
David
|
|
| |
|
| Status: |
(Mitteilung) Reaktion unnötig  | | Datum: | 17:20 Di 08.12.2009 | | Autor: | matux |
$MATUXTEXT(ueberfaellige_frage)
|
|
|
|
