Modellprüfung für temporale Logiken und gewichtete probabilistische Strukturen

• Antragstellerin: Professorin Dr. Christel Baier
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2016 bis 2024
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 289295178

Bei der Analyse von Systemen bezüglich ihrer Ressourcennutzung und anderer quantitativer Aspekte spielt die Akkumulation von Gewichten eine wichtige Rolle. So kann die Summation von nicht-negativen Gewichten (sog. Rewards) dazu dienen, den Gesamtenergieverbrauch für die Ausführung eines gegebenen Aufgabenplans oder die Gesamtkosten für verpasste Deadlines zu erfassen. Gewichtsfunktionen mit positiven und negativen Werten können beispielsweise das Energieniveau in batteriebetriebenen Geräten oder den gesamten Zugewinn oder Verlust einer Aktie an der Börse über einen Tag modellieren. Der Reihe von aktuellen Arbeiten über Temporallogiken mit Garantien für akkumulierte Gewichte folgend, ist es das Ziel des Projektes, Verifikationsprobleme für gewichtete linear- und branching-time Temporallogiken über Markov-Modellen mit diskreter Zeit und mehreren Gewichtsfunktionen zu untersuchen. Der Projektfokus wird es sein, (Fragmente von) gewichteten Temporallogiken zu identifizieren, bei denen Methoden des probabilistischen Model Checkings realisierbar sind. Speziell zielt das Projekt auf folgende Punkte ab: (1) die Untersuchung von Model-Checking Problemen für gewichtete branching-time Logiken mit Operatoren für Wahrscheinlichkeiten gewichtsbeschränkter Pfadeigenschaften und für Erwartungswerte akkumulierter Gewichte, (2) ausgefeilte Model-Checking Algorithmen für Markov-Modelle mit nicht-negativen Gewichtsfunktionen und (3) neue long-run Operatoren, die Aussagen über Scheduler mit optimalem stationären Verhalten in Markov Entscheidungsprozessen treffen. Die theoretische Arbeit wird von einer prototypischen Implementierung und experimentellen Studien begleitet.

• DFG-Verfahren: Sachbeihilfen