Sterntopologie-entkoppelte Zustandsraumsuche

• Antragsteller: Professor Dr. Jörg Hoffmann
• Fachliche Zuordnung: Bild- und Sprachverarbeitung, Computergraphik und Visualisierung, Human Computer Interaction, Ubiquitous und Wearable Computing
• Förderung: Förderung von 2016 bis 2022
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 289186625

Zustandsraumsuche ist eine Grundmethode für die Analyse großer Transitionssysteme. Zustände repräsentieren Momentaufnahmen eines Systems oder Modells zu diskreten Zeitpunkten, Transitionen repräsentieren Zustandsübergänge. Zu zeigen ist die Präsenz bzw. Absenz von Transitionspfaden mit bestimmten Eigenschaften. Solche Probleme treten in mehreren Teilgebieten der Informatik auf, insbesondere im AI Planning wo ein Agent zielführende Aktionen auswählt, und im Model Checking wo die Eigenschaften eines Programm- oder Systemmodells zu untersuchen sind. Allen Anwendungen gemeinsam ist die sog. Zustandsraumexplosion: Die Größe des Transitionssystems ist exponentiell in der Größe seiner Beschreibung.Sterntopologie-Entkopplung ist ein neuer Ansatz zur Zustandsraumreduzierung, entwickelt vom Autor für AI Planning in den Vorarbeiten zu diesem Projekt. Der Ansatz betrachtet Zustandsraum-Modelle als die Komposition eines "Zentrums" und mehrerer "Blätter", wobei das Zentrum mit jedem Blatt interagiert, die Blätter miteinander jedoch nur indirekt über das Zentrum. Solche Strukturen treten auf z.B. in Client-Server Architekturen und bei Multi-Agentensystemen mit gemeinsam genutzten Ressourcen. Die entkoppelte Suche nutzt eine Form von "bedingter Unabhängigkeit" in diesem Kontext aus: Für einen fixen Transitionspfad des Zentrums sind die möglichen zentrums-konformen Pfade der Blätter unabhängig voneinander. Die Suche kann daher eingeschränkt werden auf das Zentrum, unter Vorhaltung der zentrums-konformen Pfade für jedes Blatt separat. Dies kann die Größe des Zustandsraums exponentiell reduzieren, auch relativ zu bekannten Techniken wie Partial-Order Reduction und Petri-Netz Unfolding. Empirische Resultate zeigen substanzielle, manchmal dramatische, Verbesserungen auf Benchmarks mit augeprägter Sterntopologie. Sterntopologie-Entkopplung hat daher das Potenzial zu einer Grundmethode für effektive Zustandsraumsuche, über mehrere Informatik-Teilgebiete hinweg. Ziel des Projektes ist es, dieses Potenzial zu realisieren.Während der ersten Bewilligungsphase wurden die algorithmischen Komponenten ausgereift durch symbolische Repräsentationen, Dominanzpruning, Kombination mit Partial-Order und Symmetrie-Reduktion; die Bandbreite wurde erweitert von "Fork" Profilen zu generellen Sterntopologien; eine initiale Implementierung in SPIN Model Checking wurde durchgeführt. Die vorgeschlagene Projektverlängerung wird: (1) Die Erforschung von Basisalgorithmen abschließen durch die Ausnutzung von Sterntopologie in heuristischen Funktionen. (2) SPIN Model Checking vollständig behandeln, inklusive liveness Eigenschaften and der Kombination mit komplementären Reduktionsmethoden. (3) Die Anwendungs-Bandbreite weiter verbreitern, durch Probabilistic Model Checking auf einem Fragment der Jani Sprache, sowie durch die Anwendung auf Multi-Agentenplanung für kooperative Agenten mit gemeinsam genutzten Ressourcen.

• DFG-Verfahren: Sachbeihilfen
• Internationaler Bezug: Dänemark, Schweiz, Tschechische Republik
• Kooperationspartner: Professor Dr. Malte Helmert; Dr. Antonin Komenda; Professor Dr. Alberto Lluch-Lafuente