Das Verschmelzen von formalen Methoden und Lerntechniken für die Strategiesynthese in partiell beobachtbaren Markov-Entscheidungsprozessen

• Antragsteller: Professor Dr. Joost-Pieter Katoen
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung seit 2025
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 555465011

In diesem Projekt befassen wir uns mit dem Problem der Strategiesynthese für teilweise beobachtbare Markov-Entscheidungsprozesse (POMDPs). Obwohl dieses Problem im Allgemeinen unentscheidbar ist, gibt es in der Literatur Teillösungen unter Verwendung von semi-Algorithmen. Diese Ansätze stammen entweder von formalen Methoden, die sich auf eine partielle Entfaltung des typischerweise unendlichen Glaubensraums des POMDP stützen, oder von Lerntechniken, die Stichprobenverfahren verwenden. Formale Methoden bieten starke Garantien, lassen sich aber nicht gut auf große Systeme skalieren, während Lerntechniken größere Systeme handhaben können, aber keine robusten Korrektheitsgarantien bieten. In diesem Projekt wollen wir beide Ansätze zu einem umfassenden Rahmenwerk verschmelzen, das auf große Systeme angewendet werden kann und gleichzeitig die starken Garantien der formalen Methoden beibehält. Unsere neuen Algorithmen werden Techniken der Modellprüfung und des Lernens integrieren, einschließlich Techniken des Automatenlernens, der probabilistischen Modellprüfung, der Analyse von Gegenbeispielen, der probabilistischen Programmverfeinerung und der Monte Carlo Baumsuche mit symbolischen Hinweisen. Außerdem werden wir spezielle Fälle untersuchen, in denen die Entscheidbarkeit wiederhergestellt werden kann, insbesondere indem wir zeigen, wie Multi-Environment-MDPs und parametrische MDPs als entscheidbare Unterklassen von POMDPs betrachtet werden können.

• DFG-Verfahren: Sachbeihilfen
• Internationaler Bezug: Belgien
• Kooperationspartner: Professor Dr. Jean-Francois Raskin