Generelles Vorgehen und einfache Fälle

Worin wir Knoten bemalen

Ein Blick auf die Definition der Interpretation der Logik verrät, daß zum Bestimmen des Wertes einer zusammengesetzten Formel die Werte der Teilformeln schon vorliegen müssen. Daher kann man zwei grundlegende Wege beschreiten. Die erste, großzügige Variante berechnet, beginnend bei den Zustandsaussagen, für alle Zustände des Erreichbarkeitsgraphen die Werte der Teilformeln (bottom up). Wenn für irgendeine Zwischenformel die Berechnung läuft, kann sich die Berechnung darauf verlassen, daß der Wert von deren Teilformeln schon vorliegt und (an den Markierungen) gespeichert ist. Ein solcher Modelchecker heißt global,   weil hier am Ende der Wert edr Gesamtformel bei allen Markierungen des Erreichbarkeitsgraphen berechnet ist. Die andere Methode wertet Teilformeln nur soweit aus, wie sie in die Gesamtformel eingehen. Das entspricht mehr dem Top-Down-Prinzip. Einmal berechnete Werte werden aber trotzdem gespeichert, um Mehrfachberechnungen zu vermeiden. Diese Modelchecker heißen lokal.  . Auf den ersten Blick scheinen beide Verfahren völlig verschiedenen Aufwand zu benötigen. In Wirklichkeit lassen sich aber beide Probleme in der Zeit $O(a\cdot b)$ lösen, wobei a die Größe des Erreichbarkeitsgraphen und b die Länge der Formel ist. Das ist ein Lichtblick, denn a kann unglaublich groß werden.

Wir basteln jetzt einen lokalen Modelchecker. Wir geben uns dazu einen Erreichbarkeitsgraphen und eine Formel $\phi$ vor. Wir erfinden eine Datenstruktur, die zu jeder Markierung und (potentiell) jeder Teilformel $\phi'$von $\phi$ eine Information speichert. Diese Information besteht aus dem Wert der Teilformel und einem Bit ,,markiert``. Der Wert der Teilformel kann einer der Werte aus $\{W,F,?\}$ sein, die (dreimal dürft Ihr raten) für: $\phi'$ gilt bei m, $\phi'$ gilt bei m nicht bzw Ich habe keine Ahnung stehen. Wir adressieren die beiden Informationen durch $m.\phi'.wert$ bzw. $m.\phi'.markiert$.

Wir spendieren einen Initialisierungslauf und setzen sämtliche Informationen auf ? bzw. ,,unmarkiert``.

Der restliche Verlauf wird anhand der Formelstruktur durchgezogen. Falls die Formel eine Zustandsaussage ist, nehmen wir an, daß wir die Überprüfung locker hinbekommen. Dazu nehmen wir hier nicht weiter Stellung. Im wirklichen Leben müßten wir die zulässigen Zustandsaussagen natrlich konkret festlegen. Das täten wir halt einfach so, daß uns deren Prüfung keine Bausschmerzen bereitet.

Falls unsere Formel eine boolesche Kombination von Teilformeln ist, bestimmen wir zunächst die Werte der Teilformeln (per rekursivem Aufruf) und schauen dann in der Wahrheitswertetabelle unserer Operation nach.

Bleiben also noch die quantifizierten Temporaloperatoren. Unter diesen sind $EX \phi'$ und $AX \phi'$ auch noch einfach. Wir berechnen für alle Nachfolgezustände den Wert für $\phi'$. Wenn einer dabei ist, der $\phi'$erfüllt, ist $EX \phi'$ bei unserem Zustand auch wahr. Wenn einer dabei ist, der $\phi'$ nicht erfüllt, dann ist $AX \phi'$ bei uns auch falsch. Natürlich können wir gegebenenfalls die Berechnung der $\phi'$-Werte vorzeitig abbrechen.

Mit AF, AG, EF und EG machen wir es uns auch leicht. Es gilt nämlich

Dabei ist TRUE eine Zustandsaussage, die für alle Markierungen wahr werden soll. Es bleiben also die Konstruktionen $A(\phi U \psi)$ und $E(\phi U \psi)$.Diese sind etwas schwieriger und erfordern eigene Abschnitte. An dieser Stelle spendieren wir ihnen eigene Unterprozeduren, die wir später ausfüllen. Das heißt, daß wir nämlich jetzt schon die Modelchecking-Prozedur hinschreiben können.

Als globale Variable geben wir das Petrinetz vor. Ebenfalls global verwalten wir die Menge der schon berechneten Zustände (States). Zu jedem Zustand und jeder Teilformel der zu verifizierenden Formel tragen wir ein, ob wir deren Wert schon kennen ( bzw. 1) oder nicht ($\bullet$). Das spart wiederholte Berechnungen ein und desselben Wertes.

 

Tabelle 4.1: Modelchecking auf Erreichbarkeitsgraph