Ich frage mich, wie das genau funktioniert. Wenn Herr Valk das fragt, will er bestimmt nicht nur diesen Algorithmus mit label(s) hören, oder?

mit Model checking bezeichnet man Verfahren,
die Systemeigenschaften anhand von Zustandräumen/ -graphen? beweisen,

das funktioniert überall nur mit Algorithmen (und benötigter formaler Notation),
also auch bei Kripke-Strukturen

statt des label-Alg. kann man allgemeiner sagen,
dass Formeln der temporalen Logik (=Systemeigenschaften) gebildet werden,
die mit Hilfe des Zustandraums bewiesen werden,

ansonsten ist alles aus dem Kapitel im Zusammenhang mit der Frage
'wie funktioniert das ganze?' interessant,



äh, blabla, was war jetzt eigentlich deine Frage genau?
traf das bisherige schon irgendwie? ;)

Nun ja, im Grunde genommen war das meine Frage, aber ich wüsste jetzt nicht, wie ich ihm das anschaulich erklären könnte (möglichst nicht so allgemein gehalten… wie würde denn der Zustandsraum bei den Kripke-Strukturen aussehen? Ist das diese abgewickelte Kripke-Struktur? Und wie zeigt man das dann anhand der temporalen Logik?).

also bei dem label-Algorithmus ist es ja offensichtlich die Kripkestruktur selber,

und wenn du aus dem Stand sagen kannst,
wie du AGEFp für einen Zustand s als wahr beweisen kannst,
dann kriegst du sicher sofort ne 1

WIE weiss kein Mensch, es sei denn es gibt einen Algorithmus,
zum Beispiel der Label-Algorithmus oder die bei den Netzinvarianzeigenschaften,
das sind Möglichkeiten = Verfahren = Algorithmen um Eigenschaften zu BEWEISEN:

man schaut sich Zustände an (Markierungen dort oder atomare Formalen die dort gelten (L(s))),
man sucht von dort aus andere Zustände, vielleicht Zyklen,

das würde mir allgemein einfallen,
das wird in den angegebenen Algorithmen gemacht,

aber komplett neue/ nicht im Skript angebene Algorithmen musst du doch nicht kennen,
also ich z.B. kenn keine anderen

oder war deine Frage wie der label-Algorithmus funktioniert?