Stern-Topologie Entkoppelte Zustandsraumsuche

Abstract

Die Zustandsraumsuche ist ein weit verbreitetes Konzept in vielen Bereichen der Informatik. Die Größe der zu durchsuchenden Zustandsräume wächst jedoch typischerweise exponentiell mit der Größe einer kompakten, faktorisierten Modellbeschreibung – das ist das bekannte Problem der Zustandsexplosion. Die Entkoppelte Zustandsraumsuche (entkoppelte Suche) beschreibt einen neuartigen Ansatz um der Zustandsexplosion entgegenzuwirken. Hierfür wird die Struktur des Modells, insbesondere die bedingte Unabhängigkeit von Systemkomponenten in einer Sterntopologie, ausgenutzt. Diese Unabhängigkeit ergibt sich ganz natürlich bei vielen faktorisierten Modellen deren Zustandsräume aus dem Produkt mehrerer Komponenten bestehen. In der Dissertation wird die ent- koppelte Suche in der Planung – als Teil der Künstlichen Intelligenz (KI) – und in der Verifikation mittels Modellprüfung eingeführt. Das Konzept des entkoppelten Zustandsraums wird auf Basis von etablierten Formalismen entwickelt und seine Korrektheit bezüglich der exakten Erfassung der Erreichbarkeit von Modellzuständen bewiesen. Damit kann die entkoppelte Suche mit beliebigen Suchalgorithmen genutzt und mit komplementären Techniken kombiniert werden. In der Dissertation wird gezeigt dass die entkoppelte Suche den Suchaufwand exponentiell stärker reduzieren kann als existierende alternative Ansätze, insbesondere die Reduktion partieller Ordnung, Symmetriereduktion, Entfaltung von Petri-Netzen und symbolische Suche. Empirisch kann die entkoppelte Suche sowohl in der Planung als auch in der Modellprüfung etablierte Systeme deutlich übertreffen.