Probabilistisches Model Checking Unter teilweise Beobachtung Für Mehrere Eigenschaften

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

Probabilistisches Model Checking (PMC) ist ein Teilbereich der computergestützen Verifikation, der sich mit der automatischen Überprüfung von probabilistischen Modellen wie Markov-Entscheidungsprozesse (MDPs) beschäftigt. Das Ziel von PMC ist, für einen gegebenen MDP M und eine Spezifikation f zu überprüfen, ob M die Eigenschaft f erfüllt. Model Checker wie PRISM und Storm sind in der Lage, (viele) MDPs mit Milliarden von Zuständen innerhalb weniger Minuten zu lösen. Ein wichtiger Vorteil des PMC ist, dass eine optimale Strategie bezüglich automatisch berechnet wird. Allerdings wird bei MDPs die Annahme getroffen, dass alle Zustände vollständig beobachtbar sind. Das heißt, wenn eine endliche Folge von Zuständen und bisher ausgeführten Aktionen (die “Vorgeschichte”) gegeben ist, dann ist der aktuelle Zustand des MDP eindeutig bestimmt. In vielen realistischen Szenarien — bspw. ein Roboter mit Sensoren, die nicht die gesamte Umgebung abdecken, oder ein Angreifer, aus dessen Sicht das System eine Graybox ist — ist diese Annahme zu einschränkend. Ziel dieses Projekts ist es, die automatische Verifikation von lediglich teilweise beobachtbaren probabilistischen Modellen zu erforschen. Dies geschieht schrittweise durch die Betrachtung von immer komplexeren Modellen: Zunächst sollen MDPs, bei welchen ein Teil der Zustandsmenge beobachtbar und der andere Teil nicht beobachtbar ist, d.h. sogenannte gemischt beobachtbare MDPs (MOMDPs), untersucht werden. Danach werden partiell beobachtbare MDPs (POMDPs), bei denen der Gesamtzustand nur teilweise eingesehen werden kann betrachtet. POMDPs sind ein weitverbreitetes Modell in der Planung und der künstlichen Intelligenz. Zum Abschluss sollen partiell beobachtbare stochastische Spiele (POSGs), die eine Verallgemeinerung von POMDPs durch einen weiteren Spieler darstellen, untersucht werden. Hierbei soll das Hauptaugenmerk auf Spezifikationen, welche aus mehreren Eigenschaften zusammengesetzt sind, liegen. Ein Beispiel einer solchen Spezifikation ist in etwa, dass gewisse Zielzustände mit hoher Wahrscheinlichkeit erreicht werden sollen, während gleichzeitig Fehlerzustände immer vermieden werden. Als Vorbereitung dazu sollen zunächst einige offene Fragen bezüglich derartiger Multi-Eigenschaften in MDPs betrachtet werden. Je nachdem, welcher Modelltyp gegeben ist, sollen verschiedene Typen von Multi-Eigenschaften untersucht werden. Dies umfasst u.a. Mischungen von stochastischen und nicht-stochastischen (z.B. für alle/es existiert) Eigenschaften, mehrere Einzelspezifikationen mit lexikographischer Ordnung, erwartete Kosten bezüglich einer mehrdimensionalen Kostenfunktion, sowie Spezifikationen, die sich auf vollständig oder partiell beobachtbare Zustände beziehen. Diese Untersuchungen werden sich auf die Entscheidbarkeit und Komplexität, sowie auf die Entwicklung von (approximativen) Algorithmen und deren Implementierung und experimentelle Auswertung im Model Checker Storm konzentrieren.

• DFG-Verfahren: Sachbeihilfen