Wie liest man eine Reihe von atomaren Aussagen?

Question

Ich habe das obige System für atomare Aussagen {a, b, c} gegeben.

Ich soll dann sagen, ob bestimmte LTL Formeln halten (wie ♢☐c).

Ich verstehe, was die LTL-Formeln bedeuten (schließlich für immer c hält), aber ich habe keine Ahnung, wie man das Diagramm liest und es auf die LTL beziehen.

Ich nehme an, es ist wie ein Flussdiagramm in dem wir von oben links beginnen, /{a} und können durch die verschiedenen Zustände gehen. Aber was bedeutet jedes davon geteilt durch a?

Answer 1

Sieht aus wie FSM/Transducer und nicht eine Kripke-Struktur. Eingabe/Ausgabe oder allgemeiner Vorbedingung/Nachbedingung ist eine gemeinsame Notation für FSM und seine Verwandten. Vorbedingung/Nachbedingung (a and b and ...)/(x and y and...). So a im Staat q1. In nächsten Zuständen entweder nur b in Q4 oder b and c oder Q3. Könnte natürlich or anstelle von and in Vorbedingung sein, sonst könnte das System anhalten ..