Temporal Logics and Probabilistic Model Checking for Weighted Structures
Final Report Abstract
Automaton models with weight annotations for states or transitions are widely used as operational models for system analysis with respect to resource consumption and cost-benefit trade-offs. In the literature, various modal logics have been introduced to formalize requirements on accumulated weights along (fragments of) computation paths. For instance, the accumulation of non-negative weights can represent the total energy consumption of a task schedule or the total penalty incurred for missed deadlines, while weight functions with both negative and positive values can be used to model energy levels in batterypowered devices or the total profit or loss of a stock over a trading day. A key objective of the project was to investigate verification problems for discrete-time Markov models with one or more weight functions. The central preliminary work of the project proposal was a paper from 2014, which introduces an extension of linear temporal logic (LTL) with modalities for weight accumulation under regular side conditions and examines aspects of expressiveness, as well as the boundary between decidability and undecidability of the model-checking problem for finite transition systems, Markov chains, and Markov decision processes (MDPs) with multiple weight functions. The project focused on the following topics: (1) the investigation of model-checking problems for a branching-time logic defined analogously, which extends probabilistic computation tree logic (PCTL) with operators for the probabilities of weight-dependent path properties, (2) a prototype implementation of the algorithms from the paper as well as the algorithms developed in (1) and experimental studies, (3) algorithms for expectations of accumulated weights, particularly variants of the classical stochastic shortest-path problem, (4) algorithms for new long-run operators to formalize properties of the stationary behavior of MDPs.
Publications
-
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
