Implementation der Suche für den AU-Operator

Worin wir Gegenbeispiele suchen

Wir schauen uns im gesamten Abschnitt die Formel $A(\phi U \psi)$ an und wollen deren Wert bei der Markierung m bestimmen. Da kann es erstmal nicht schaden, sich die Werte von $\phi$ und $\psi$ bei m anzusehen. Wenn $m \models \psi$, dann ist ja ohne Suchen alles klar, dann gilt auch $m \models A(\phi U \psi)$. Wenn $m \not\models\psi$ und $m \not\models \phi$, dann ist ebenfalls alles klar, es gilt definitiv $m \not\models A(\phi U \psi)$. Wozu also suchen? Ah ja: da ist ja noch der Fall $m \models \phi$ und $m \not\models\psi$.

Tiefensuche liefert auf natürliche Weise einen Pfad. Also ist es besser, die Aussage über alle Pfade (AU) in eine Aussage über einen Pfad zu übersetzen. Das geschieht, indem wir versuchen, die Formel zu widerlegen. Gelingt das, ist die Formel falsch, gelingt das nicht, müssen wir sicher sein, daß wir so intensiv gesucht haben, daß es auch wirklich kein Gegenbeispiel gibt, die Formel also gilt.

Wie sieht nun ein Gegenbeispiel aus. Auf keinen Fall darf $\psi$irgendwo gelten. Eine Möglichkeit $\phi U \psi$ zu widerlegen, ist nun, daß irgendwann $\phi$ nicht mehr und $\psi$ noch nicht gilt. Das ist ein Pfad, wo auf allen Knoten außer dem letzten $\phi$ und $\neg \psi$ gilt und auf dem letzten $\neg \phi$ und $\neg \psi$.Die andere Möglichkeit ist, daß der Pfad unendlich lang ist und $\phi$die ganze Zeit gilt. Das heißt, alle Elemente des Pfades erfüllen $\phi$ und $\neg \psi$. Einen unendlichen Pfad erkennen wir daran, daß sich Knoten wiederholen, wir also einen Zyklus finden. Anders kann man auf einem endlichen Graphen nicht unendlich lange laufen. Die beiden Möglichkeiten, Gegenbeispiele zu bilden, drückt folgende Äquivalenz aus:

$$\neg A(\phi U \psi) \iff EG (\phi \wedge \neg \psi) \vee E(\neg \psi U (\neg \phi \wedge \neg \psi))$$

Technisch gesehen, gibt es eine dritte Art Gegenbeispiel. Wenn wir nämlich bei der Suche einen Knoten finden, für den wir den Wert von $A(\phi U \psi)$schon kennen (aufgrund irgendeiner früheren Berechnung), dann gibt es zwei Möglichkeiten: Wenn die Formel dort gilt, kann auch unser aktueller Pfad nicht zu einem Gegenbeispiel verlängert werden. Gilt die Formel dort nicht, kann unser Pfad mit dem dortigen Gegenbeispiel verkettet werden, wir können also unseren aktuellen Pfad als Gegenbeispiel auffassen.

Wir beobachten, daß wir nur von denjenigen Knoten weitersuchen müssen, die $\phi$ und $\neg \psi$ erfüllen. Sobald unser Pfad in einen Knoten mit anderen Werten für $\phi$ und $\psi$ einmündet, steht der Wert von $\phi U \psi$ für diesen Pfad fest. Wir suchen also in dem Teich der Markierungen, die $\phi$ und $\neg \psi$ erfüllen und dessen Ufern. Wir brechen die Suche ab, sobald ein Gegenbeispiel gefunden ist, d.h. wir einen weissen Knoten betreten haben, der weder $\phi$ noch $\psi$erfüllt, oder einen Kreis gefunden haben, also bei der Suche auf einen bereits grauen Knoten stoßen, oder einen Knoten mit schon bekanntem Gegenbeispiel finden. Finden wir kein Gegenbeispiel, gilt die Formel, und zwar für alle Knoten, die bei der Suche tangiert wurden.

Wenn wir einen Gegenbeispielpfad finden, dann müssen wir allen grauen und schwarzen Knoten einen Wert zuordnen. F'ur graue Knoten ist das einfach. Die liegen auf dem Gegenbeispielpfad und der bei ihnen beginnende Teilpfad ist in jedem Falle ein Gegenbeispielpfad. Bleiben die schwarzen Knoten. Von denen ausgehend wurde offenbar weder ein Kreis noch eine Markierung, wo $\neg \phi$und $\neg \psi$ gilt, gefunden. Ein Gegenbeispielpfad eines schwarzen Knotens k müßte also über einen grauen Knoten k' führen. Nun ist aber k von irgendeinem grauen Knoten (mindestens von k₀ aus) erreichbar. Es sei k'' der Knoten mit der größten dfs in Grau, von dem aus k erreichbar ist. Da k' noch in Grau ist, aber von k erreichbar, muß k' schon in Grau gewesen sein, als Expand(k'') gerufen wurde (Eigenschaft (4) der Tiefensuche). Also sind erreichbar: k'' von k' (graue Knoten bilden einen Weg), k von k'' und k' von k. Wenn das man kein Kreis ist! Und demnach ein Gegenbeispiel, das wir hätten viel früher finden müssen! Da wir dieses Gegenbeispiel aber nicht gefunden haben, müssen wir unsere Annahme, zu schwarzen Knoten gäbe es ein Gegenbeispiel, zurücknehmen. Das heißt, schwarze Knoten bekommen beim Finden eines Gegenbeispielpfades den Wert TRUE für $A(\phi U \psi)$.

  

Abbildung 4.1: Schwarze Knoten haben kein Gegenbeispiel

Zusammengefaßt: Ist ein Gegenbeispielpfad gefunden, gilt die Formel für alle schwarzen Knoten, und sie gilt für keinen grauen Knoten. Die weissen brauchen wir nicht zu beschriften. Also kann CheckAU als einfache Adaption von DFS programmiert werden. Wir müssen nur die Berechnung der Nachfolger durch das Schalten von Transitionen ersetzen und Knoten geeignet mit den richtigen Ergebnissen der Formelauswertung versehen. Die Menge Weiss ist implizit durch die Menge der schon berechnneten und noch nicht berechneten Zustände gegeben. Im folgenden Algorithmus schreibe ich alles normal, was kanonisch zur Tiefensuche gehört (inklusive Nachfolgerberechnung) und kennzeichnen mit einem Plus, was für unsere Adaption spezifisch ist. Für CheckAU benötigen wir die min-Information gar nicht, weil die Farbzuordnung für Knoten nicht davon abhängt. Wir schreiben vor die entsprechenden Zeilen ein Minus zum Zeichen, daß man sie weglassen kann.

 

Tabelle 4.3: Auswertung von AU-Formeln

 

Tabelle 4.4: Fortsetzung von CheckAU

Das isses also.