Erstens: welcher Algorithmus aus dem Abschnitt 5.7.4 ist da gemeint??
Zweitens: Wie werden Verifikationen der Semantik und Syntax von CTL-Formeln durchgeführt?

Auf 12.2.2 : Welcher Algo ist denn hier wieder gemeint. Die sind doch im Skript alle schön durchnummeriert. Warum hat man die Nummer nicht direkt angegeben, sondern das Versteckspiel mit Abschnitten???

Zu erstens (sowohl 12.2.1 als auch 12.2.2): "Der Algorithmus in Abschnitt 5.7.4" ist nicht über seine Nummer referenziert, weil er keine Nummer hat.  Seine Beschreibung füllt die ersten drei bis vier Seiten des genannten Abschnittes.

Zu zweitens: Die Formulierung der Frage spricht nicht dafür, dass der Begriff 'Verifikation' vom Verfasser verstanden wurde.  Die Syntax legt fest, was wohlgeformte CTL-Formeln sind.  Die Semantik legt fest, unter welchen Bedingungen eine CTL-Formel erfüllt ist. Wenn man beides hat, kann man CTL-Formeln im Rahmen der Verifikation einsetzen.

Ich meinte nicht die Verifikation vom Kapitel 5 (also das Einsatzgebiet von CTL-Formeln), sondern die Verifikation der Richtigkeit einer CTL-Formel. Damit sie sich eine CTL-Formel nennen darf, muss sie bestimmen syntaktischen Kriterien genügen.

Abpropos Syntax von CTL-Formeln:  Ich bekam per Mail folgende Frage (sinngemäß zitiert):

Bei Aufgabe 12.2.2 fällt bei der Formel am Anfang das ¬E auf!
Handelt es sich dabei möglicherweise nicht um eine CTL-Formel, da nach dem E kein Pfadquantor X, F, G oder U folgt?

Antwort: Doch, die Formel ist in CTL wohlgeformt, auf den Zustandsquantor E folgt der Pfadquantor U.  Der wird allerdings in Infix-Notation zwischen seine beiden Teilformeln geschrieben, daher ist das erst ersichtlich, wenn man die Klammerung beachtet.

Zur Prüfung der syntaktischen Korrektheit gibt es kein spezielles Verfahren. Die wohlgeformten CTL-Formeln sind durch eine kontextfreie Grammatik in Backus-Naur-Form beschrieben. Ob eine Formel von der Grammatik erzeugt werden kann, ist mit den üblichen Verfahren aus FGI-1 feststellbar.

Ich habe nun die Aufgabe durchgerechnet und bekam als Endergebnis {1,2}. Kann das hinhauen?
Was sollen wir eigentlich in die Kästchen (Zustände) malen? Pünktchen, um die Zustände zu markieren, die das jeweilige Prädikat erfüllen?

Hat denn keiner die Aufgabe bisher durchgerechnet??

die atome heißen doch
Close
Heat
Error
Diese werden doch in der Zeichnung mit C H und E abgekürzt und zeigen an, welche in welchem Zustand zutreffen bzw ein - wenn sie nicht zutreffen.
Meine Frage:
wofür steht das S ??

Start? Siehe Abbildung 5.24

zu 12.2.2

habe f in teilformeln zerlegt, angefangen bei den atomen, und diese eingezeichnet, und nach und nach erweitert, bis ich dann f hatte.habe komischerweise nur 7 der 8 abbildungen benötigt.
habe auch (1,2) raus, wobei das ergebnis wohl nicht so die rolle spielt, da es ja drauf ankommt die teilformeln richtig einzuzeichnen und zu erweitern.
ich habe einfach die felder schraffiert, die zur jeweiligen teilformel gehören, denke mal, das man es so machen soll. ob (1,2) als endergebnis richtig ist, weiß ich nicht, da ich nur 7 der 8 abbildungen benutzt habe, und es somit sein kann das ich irgendeine teilformel übersehen habe. wenn nicht korrigiert mich

In irgendeiner Übungsgruppe soll wohl gesagt worden sein, dass man es falsch gemacht habe, wenn man alle acht Abbildungen gebraucht habe. Ich persönlich habe (so wie der Algorithmus es m.E. vorschreibt) alle auftretenden Teilformeln eingezeichnet und habe damit insgesamt zwölf Diagramme gebraucht. Wenn man die drei vorkommenden atomaren Formeln nicht einzeichnet, blieben noch neun. Vielleicht sollte man die Negationen immer sofort dazunehmen? Mal sehen, wie die Musterlösung aussieht.

In irgendeiner Übungsgruppe soll wohl gesagt worden sein, dass man es falsch gemacht habe, wenn man alle acht Abbildungen gebraucht habe.

Das war dann wohl ich. Aber eigentlich meine ich, mich sofort korrigiert zu haben… Die Aussage war, dass die Formel nicht in allen Zuständen zutrifft.

Ich persönlich habe (so wie der Algorithmus es m.E. vorschreibt) alle auftretenden Teilformeln eingezeichnet und habe damit insgesamt zwölf Diagramme gebraucht. Wenn man die drei vorkommenden atomaren Formeln nicht einzeichnet, blieben noch neun. Vielleicht sollte man die Negationen immer sofort dazunehmen? Mal sehen, wie die Musterlösung aussieht.

Die Atome und ihre Negationen sind doch schon durch die Buchstaben bzw. Striche angedeutet… zumindest wars so gedacht.

Ich brauchte genau 8 Abbildungen (also Zwischenschritte). Es passt bei mir wie die Faust aufs Auge. Es kann sein, dass ihr die Teilformel (nicht)EGClose als ein Schritt verarbeitet habt; bei mir sind es definitiv zwei.

Wie UncleOwen schon sagte, die Atome sind durch die Striche über den Kreisen eingezeichnet, so z.B. heißt "-CH-" (nicht)StartCloseHeat(nicht)Error

Man muss dann nur noch auf irgend eine Weise die Zustände(Kreise) markieren, um zu zeigen, dass die jeweilige Teilformel in den markierten Zuständen gültig ist (das Prädikat erfüllt).