51 citations · 233 across the 33 of their papers we have counts for
38 papers
Property-driven Causal Abstractions for Markov Decision Processes
Jule Schmidt, Maximilian Weininger, Clemens Dubslaff +2
Markov Decision Processes (MDPs) are widely used as decision-making models, commonly specified over factored state spaces through state variables and their valuations. The exponent…
dtControl2+: Trading Optimality for Explainability in MDPs via Decision Trees
Tereza Kinská, Jan Křetínský, Tobias Meggendorfer +2
Over the past decade, decision trees have been used to represent controllers (a.k.a. policies) in an explainable way, with dtControl2 as a current state-of-the-art tool. However, f…
Confidence Sequences for Online Statistical Model Checking of Markov Decision Processes
Konstantin Kueffner, Tobias Meggendorfer, Maximilian Weininger +1
Markov decision processes (MDPs) are a classic model of decision making under uncertainty, exhibiting both non-deterministic choice as well as probabilistic uncertainty. Traditiona…
UMB: A Unified Markov Binary Format for Probabilistic Model Checking (extended version)
Roman Andriushchenko, Arnd Hartmanns, Joshua Jeppson +5
This paper presents the unified Markov binary (UMB) format, an efficient, extensible, and well-supported explicit-state file format for representing a wide range of probabilistic s…
Missingness-MDPs: Bridging the Theory of Missing Data and POMDPs
Joshua Wendland, Markel Zubia, Roman Andriushchenko +6
We introduce missingness-MDPs (miss-MDPs), a novel subclass of partially observable Markov decision processes (POMDPs) that incorporates the theory of missing data. A miss-MDP is a…
Perception-Based Beliefs for POMDPs with Visual Observations
Miriam Schäfers, Merlijn Krale, Thiago D. Simão +2
Partially observable Markov decision processes (POMDPs) are a principled planning model for sequential decision-making under uncertainty. Yet, real-world problems with high-dimensi…
Sound Value Iteration for Simple Stochastic Games
Muqsit Azeem, Jan Kretinsky, Maximilian Weininger
Algorithmic analysis of Markov decision processes (MDP) and stochastic games (SG) in practice relies on value-iteration (VI) algorithms. Since basic VI does not provide guarantees…
Statistical Model Checking Beyond Means: Quantiles, CVaR, and the DKW Inequality (extended version)
Carlos E. Budde, Arnd Hartmanns, Tobias Meggendorfer +2
Statistical model checking (SMC) randomly samples probabilistic models to approximate quantities of interest with statistical error guarantees. It is traditionally used to estimate…
Risk-aware Markov Decision Processes Using Cumulative Prospect Theory
Thomas Brihaye, Krishnendu Chatterjee, Stefanie Mohr +1
Cumulative prospect theory (CPT) is the first theory for decision-making under uncertainty that combines full theoretical soundness and empirically realistic features [P.P. Wakker…
Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games
Marta Grobelna, Jan Křetínský, Maximilian Weininger
We consider two-player zero-sum concurrent stochastic games (CSGs) played on graphs with reachability and safety objectives. These include degenerate classes such as Markov decisio…
Fixed Point Certificates for Reachability and Expected Rewards in MDPs
Krishnendu Chatterjee, Tim Quatmann, Maximilian Schäffeler +3
The possibility of errors in human-engineered formal verification software, such as model checkers, poses a serious threat to the purpose of these tools. An established approach to…
Solving Robust Markov Decision Processes: Generic, Reliable, Efficient
Tobias Meggendorfer, Maximilian Weininger, Patrick Wienhöft
Markov decision processes (MDP) are a well-established model for sequential decision-making in the presence of probabilities. In robust MDP (RMDP), every action is associated with…
Sound Value Iteration for Simple Stochastic Games
Muqsit Azeem, Jan Kretinsky, Maximilian Weininger
Algorithmic analysis of Markov decision processes (MDP) and stochastic games (SG) in practice relies on value-iteration (VI) algorithms. Since the basic version of VI does not prov…
Sound Statistical Model Checking for Probabilities and Expected Rewards (extended version)
Carlos E. Budde, Arnd Hartmanns, Tobias Meggendorfer +2
Statistical model checking estimates probabilities and expectations of interest in probabilistic system models by using random simulations. Its results come with statistical guaran…
1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization
Muqsit Azeem, Debraj Chakraborty, Sudeep Kanav +4
Despite the advances in probabilistic model checking, the scalability of the verification methods remains limited. In particular, the state space often becomes extremely large when…
Tools at the Frontiers of Quantitative Verification
Roman Andriushchenko, Alexander Bork, Carlos E. Budde +20
The analysis of formal models that include quantitative aspects such as timing or probabilistic choices is performed by quantitative verification tools. Broad and mature tool suppo…
Playing Games with your PET: Extending the Partial Exploration Tool to Stochastic Games
Tobias Meggendorfer, Maximilian Weininger
We present version 2.0 of the Partial Exploration Tool (PET), a tool for verification of probabilistic systems. We extend the previous version by adding support for stochastic game…
What Are the Odds? Improving the foundations of Statistical Model Checking
Tobias Meggendorfer, Maximilian Weininger, Patrick Wienhöft
Markov decision processes (MDPs) are a fundamental model for decision making under uncertainty. They exhibit non-deterministic choice as well as probabilistic uncertainty. Traditio…
Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives
Jan Křetínský, Tobias Meggendorfer, Maximilian Weininger
A classic solution technique for Markov decision processes (MDP) and stochastic games (SG) is value iteration (VI). Due to its good practical performance, this approximative approa…
A Practitioner's Guide to MDP Model Checking Algorithms
Arnd Hartmanns, Sebastian Junges, Tim Quatmann +1
Model checking undiscounted reachability and expected-reward properties on Markov decision processes (MDPs) is key for the verification of systems that act under uncertainty. Popul…
Algebraically Explainable Controllers: Decision Trees and Support Vector Machines Join Forces
Florian Jüngermann, Jan Křetínský, Maximilian Weininger
Recently, decision trees (DT) have been used as an explainable representation of controllers (a.k.a. strategies, policies, schedulers). Although they are often very efficient and p…
Optimistic and Topological Value Iteration for Simple Stochastic Games
Muqsit Azeem, Alexandros Evangelidis, Jan Křetínský +2
While value iteration (VI) is a standard solution approach to simple stochastic games (SSGs), it suffered from the lack of a stopping criterion. Recently, several solutions have ap…
Satisfiability Bounds for -Regular Properties in Bounded-Parameter Markov Decision Processes
Jan Křetínský, Tobias Meggendorfer, Maximilian Weininger
We consider the problem of computing minimum and maximum probabilities of satisfying an -regular property in a bounded-parameter Markov decision process (BMDP). BMDP arise from…
Stochastic Games with Disjunctions of Multiple Objectives
Tobias Winkler, Maximilian Weininger
Stochastic games combine controllable and adversarial non-determinism with stochastic behavior and are a common tool in control, verification and synthesis of reactive systems faci…