9 citations · 26 across the 15 of their papers we have counts for
7 papers · 1 filter
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…
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…
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…
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…