51 citations · 233 across the 33 of their papers we have counts for
5 papers · 1 filter
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…