Sterntopologie-entkoppelte Zustandsraumsuche
Zusammenfassung der Projektergebnisse
Die Planung ist einer der grundlegenden Teilbereiche der KI. Ihre Technologie ermöglicht es jedes Problem zu lösen das durch die Suche nach Pfaden in grossen Zustandsräumen modelliert werden kann und kann die Problemlösung drastisch vereinfachen: Anstelle von 1000en Zeilen Programmcode schreibt/unterhält man wenige dutzend Zeilen Modellcode. Ein Haupthindernis bei der Entwicklung von Planungssystemen die mit grosen Probleminstanzen umgehen können, ist das Problem der Zustandsexplosion. Ein kompaktes Modell beschreibt hier einen Zustandsraum dessen Größe exponentiell mit der Größe des Modells wächst. In den letzten Jahrzehnten wurden viele Techniken entwickelt, die das Problem der Zustandsexplosion angehen. Die in diesem Projekt entwickelte Stern-Topologie entkoppelte Zustandsraumsuche ist eine neue Ergänzung dieser Techniken. Die entkoppelte Suche zerlegt eine gegebene faktorisierte Modelldarstellung, d.h. Zustandsvariablen in der Planung oder synchronisierte Automaten in der Modellprüfung, um die bedingte Unabhängigkeit von Teilen des Modells auszunutzen. Auf diese Weise vermeidet die entkoppelte Suche die Explosion die sich aus der Aufzählung aller möglichen Kombinationen von Zuweisungen zu diesen unabhängigen Teilen ergibt. Dies geschieht indem nur über Sequenzen von Übergängen gesucht wird die Komponenten synchronisieren und gleichzeitig für jede Blattkomponente die Menge der entlang dieser synchronisierenden Übergangssequenz erreichbaren Komponentenzustände aufgezählt wird. Im Rahmen des Projekts wurde die entkoppelte Suche im Kontext der klassischen KI-Planung und der Modellprüfung entwickelt. Im Anschluss an zwei erste Arbeiten, die vor dem Projekt von der Forschungsgruppe des Projektleiters veröffentlicht wurden, wurde das Thema deutlich vertieft. Ein wesentlicher Bestandteil ist der Vergleich mit bestehenden Arbeiten, die zuvor zur Bewältigung des Problems der Zustandsexplosion eingeführt wurden. Als ein Hauptergebnis des Projekts stellte sich heraus, dass die entkoppelte Suche orthogonal zu allen bekannten Techniken zur Reduktion des Zustandsraums ist, insbesondere zu den Methoden zur Reduktion partieller Ordnungen, zur Symmetriereduktion, zur symbolischen Zustandsdarstellung und zur Petri-Netz-Entfaltung. Die entkoppelte Suche wurde als Ansatz zur Lösung von Planungsproblemen mittels heuristischer Suche, der derzeit beliebtesten Methode zur Lösung solcher Probleme, auf dem aktuellen Stand der Technik etabliert. Die Eigenschaften des entkoppelten Zustandsraums wurden eingehend untersucht, was zu einem gut funktionierenden Planungssystem führte. Im Rahmen der ersten Projektphase wurden, aufbauend auf der Orthogonalität der entkoppelten Suche zu bestehenden Ansätzen, Anpassungen mehrerer dieser Methoden an den entkoppelten Zustandsraum entwickelt, was zu Suchalgorithmen führte, die die Vorteile beider Methoden in sich vereinen. In der Modellprüfung wurde die entkoppelte Suche sehr erfolgreich auf die Verifizierung von Sicherheits- und Lebendigkeitseigenschaften angewandt. Das resultierende Tool übertrifft den SPIN-Modellprüfer auf Instanzen mit mehreren interagierenden Modellkomponenten. Der wissenschaftliche Output des Projekts ist ein voller Erfolg: Die Gruppe des Projektleiters veröffentlichte 2 Beiträge in wichtigen Fachzeitschriften und 14 Beiträge auf wichtigen internationalen Konferenzen zu den Projektthemen.
