Modellprüfung für temporale Logiken und gewichtete probabilistische Strukturen
Zusammenfassung der Projektergebnisse
Automatenmodelle mit Gewichtsannotationen für die Zustände oder Transitionen sind als operationelle Modelle für die Systemanalyse hinsichtlich des Ressourcenverbrauchs und Kosten-Nutzen-Verhältnissen weit verbreitet. In der Literatur wurden verschiedene Logiken mit Modalitäten, mit denen sich Anforderungen an akkumulierte Gewichte entlang von (Fragmenten von) Berechnungspfaden formalisieren lassen, eingeführt. Zum Beispiel kann die Akkumulation nicht negativer Gewichte zur Formalisierung des Gesamtenergieverbrauchs eines Aufgabenplans oder der Gesamtstrafe, die bei Fristüberschreitungen zu zahlen ist, dienen, während Gewichtsfunktionen mit negativen und positiven Werten zur Modellierung des Energieniveaus in batteriebetriebenen Geräten oder des Gesamtgewinns oder -verlusts einer Aktie an einem Börsentag verwendet werden können. Wesentliches Ziel des Projektes war es, Verifikationsprobleme für zeitdiskrete Markovmodelle mit einer oder mehreren Gewichtsfunktionen zu untersuchen. Die zentrale Vorarbeit des Projektantrags war ein Paper von 2014, das eine Erweiterung der Temporallogik LTL (linear temporal logic) um Modalitäten für die Gewichtsakkumulation unter regulären Seitenbedingungen vorstellt und Aspekte der Ausdrucksstärke sowie die Grenze zwischen Entscheidbarkeit und Unentscheidbarkeit des Modellprüfungsproblems für endliche Transitionssysteme, Markovketten und Markov Entscheidungsprozesse (engl. Abkürzung MDPs) mit mehreren Gewichtsfunktionen untersucht. Die Schwerpunkte des Projekts lagen auf folgenden Fragestellungen: (1) der Untersuchung von Modellprüfungsproblemen für eine Branching-Time-Logik, die die Logik PCTL (probabilistic computation tree logic) um Operatoren für die Wahrscheinlichkeiten gewichtsabhängiger Pfadeigenschaften erweitert, (2) eine prototypische Implementierung der Algorithmen des Papers sowie der in (1) entwickelten Algorithmen und experimentelle Studien, (3) Algorithmen für Erwartungswerte akkumulierter Gewichte, insbesondere Varianten des klassischen stochastischen Kürzeste-Wege-Problems, (4) Algorithmen für neue Long-Run-Operatoren, mit denen sich Eigenschaften zum stationären Verhalten von MDPs formalisieren lassen.
Projektbezogene Publikationen (Auswahl)
-
Greener Bits: Formal Analysis of Demand Response. Lecture Notes in Computer Science, 323-339. Springer International Publishing.
Baier Christel; Klüppelholz Sascha; de Meer Hermann; Niedermeier Florian & Wunderlich Sascha
-
Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Büchi automata. International Journal on Software Tools for Technology Transfer, 20(2), 179-194.
Klein, Joachim; Baier, Christel; Chrszon, Philipp; Daum, Marcus; Dubslaff, Clemens; Klüppelholz, Sascha; Märcker, Steffen & Müller, David
-
Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes. Lecture Notes in Computer Science, 160-180. Springer International Publishing.
Baier Christel; Klein Joachim; Leuschner Linda; Parker David & Wunderlich Sascha
-
Maximizing the Conditional Expected Reward for Reaching the Goal. Lecture Notes in Computer Science, 269-285. Springer Berlin Heidelberg.
Baier Christel; Klein Joachim; Klüppelholz Sascha & Wunderlich Sascha
-
Towards Automated Variant Selection for Heterogeneous Tiled Architectures. Lecture Notes in Computer Science, 382-399. Springer International Publishing.
Baier Christel; Klüppelholz Sascha & Wunderlich Sascha
-
Bisimulations, logics, and trace distributions for stochastic systems with rewards. Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), 31-40. ACM.
Gburek, Daniel & Baier, Christel
-
Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes. Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 86-94. ACM.
Baier, Christel; Bertrand, Nathalie; Dubslaff, Clemens; Gburek, Daniel & Sankur, Ocan
-
Stochastic transition systems: bisimulation, logic, and composition. Doktorarbeit, Technische Universität Dresden, Germany, 2018
Daniel Gburek
-
Long-run Satisfaction of Path Properties. 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1-14. IEEE.
Baier, Christel; Bertrand, Nathalie; Piribauer, Jakob & Sankur, Ocan
-
Partial and Conditional Expectations in Markov Decision Processes with Integer Weights. Lecture Notes in Computer Science, 436-452. Springer International Publishing.
Piribauer, Jakob & Baier, Christel
-
On Skolem-hardness and saturation points in Markov decision processes. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming, (ICALP), volume 168 of LIPIcs, pages 138:1–138:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020
Jakob Piribauer & Christel Baier
-
On non-classical stochastic shortest path problems. Doktorarbeit, Technische Universität Dresden, Germany, 2021
Jakob Piribauer
-
The variance-penalized stochastic shortest path problem. In Mikolaj Bojanczyk, Emanuela Merelli, and David P. Woodruff, editors, 49th International Colloquium on Automata, Languages, and Programming (ICALP), volume 229 of LIPIcs, pages 129:1–129:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022
Jakob Piribauer, Ocan Sankur & Christel Baier
-
Effectiveness of Pre-computed Knowledge in Self-adaptation - A Robustness Study. Lecture Notes in Computer Science, 19-34. Springer International Publishing.
Korn, Max; Chrszon, Philipp; Klüppelholz, Sascha; Baier, Christel & Wunderlich, Sascha
-
Entropic risk for turn-based stochastic games. In Jérôme Leroux, Sylvain Lombardy, and David Peleg, editors, 48th International Symposium on Mathematical Foundations of Computer Science, MFCS 2023, August 28 to September 1, 2023, Bordeaux, France, volume 272 of LIPIcs, pages 15:1–15:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
Christel Baier, Krishnendu Chatterjee, Tobias Meggendorfer & Jakob Piribauer
-
Probabilistic Model Checking for Temporal Logics in Weighted Structures. Doktorarbeit, Technische Universität Dresden, Germany, 2024
Sascha Wunderlich
-
Risk-averse optimization of total rewards in Markovian models using deviation measures. In Rupak Majumdar and Alexandra Silva, editors, 35th International Conference on Concurrency Theory (CONCUR), LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
Christel Baier, Jakob Piribauer & Maximilian Starke
