96 research outputs found
Multi-objective Optimization of Long-run Average and Total Rewards: Supplemental Material
No full textSupplemental Material for the Paper:
Multi-objective Optimization of Long-run Average and Total Rewards
by Tim Quatmann and Joost-Pieter Katoen
Experimental Results for Sound Value Iteration
No full textThis file contains the experimental results for the paper"Sound Value Iteration"by Tim Quatmann and Joost-Pieter Katoen presented at CAV 2018.- The directory ./models contains all model files (in the PRISM input language) and the corresponding properties that were considered in the paper.- The directory ./logs/ contains all obtained logfiles, i.e., the output generated by Storm and Prism, respectively.- The file ./data.csv lists model checking times and the number of performed iterations as extracted from the logfiles
Multi-objective Optimization of Long-run Average and Total Rewards: Supplemental Material
No full textSupplemental Material for the Paper:
Multi-objective Optimization of Long-run Average and Total Rewards
by Tim Quatmann and Joost-Pieter Katoen.
This artifact contains our implementation for the paper "Multi-objective Optimization of Long-run Average and Total Rewards". The implementation is fully integrated into the model checker Storm.
We include the sources and dependencies of Storm as well as the related tools MultiGain and PRISM-games.
Moreover, we include model files and scripts for replicating *all* experiments as conducted for the paper.
The original logfiles obtained during our experiments are included as well.
The artifact has been tested to work with the TACAS 21 Artifact Evaluation VM running Ubuntu 20.04 LT
The Probabilistic Model Checker Storm: Evaluation Results and Replication Package
No full textThis package contains logdata and replication scripts for the evaluation of the model checker Storm (www.stormchecker.org) as part of the paper:
"The Probabilistic Model Checker Storm" by Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, and Matthias Volk</p
Artifact for Paper: Under-Approximating Expected Total Rewards in POMDPs
No full textSupplemental Material for the Paper:
Under-Approximating Expected Total Rewards in POMDPs
by Alexander Bork, Joost-Pieter Katoen, and Tim Quatmann.
This artifact contains the implementation for the paper "Under-Approximating Expected Total Rewards in POMDPs". Our implementation is part of the probabilistic model checker Storm.
Included are the source files of Storm with the extensions we made and all required dependencies. Furthermore, we include the sources of the model checker PRISM which we used as a comparison.
In addition to the tools, the artifact contains the model files we used for evaluating our implementation and scripts to replicate the experiments we conducted for the paper automatically.
Furthermore, we include scripts to run a subset of the experiments for a less time intensive evaluation of the implementation.
For validation of our original experiments, the original logfiles are also included.
The artifact has been tested to work with the TACAS 22 Artifact Evaluation VM running Ubuntu 20.04 LT
A Spectrum of Approximate Probabilistic Bisimulations
No full textThis paper studies various notions of approximate probabilistic bisimulation on labeled Markov chains (LMCs). We introduce approximate versions of weak and branching bisimulation, as well as a notion of ε-perturbed bisimulation that relates LMCs that can be made (exactly) probabilistically bisimilar by small perturbations of their transition probabilities. We explore how the notions interrelate and establish their connections to other well-known notions like ε-bisimulation
Riding the Storm in a Probabilistic Model Checking Landscape
No full textProbabilistic model checking is a formal verification technique to check whether stochastic models satisfy properties of interest. Along with a rich theory, the community has developed mature tool support, which in turn has been applied to a set of industrial case studies. This paper demonstrates various abilities of the probabilistic model checker Storm by a set of simple and more accessible examples.</p
What is the Best Algorithm for MDP Model Checking? Replication Package
No full textThis artefact allows to review and replicate the experiments from the paper What is the Best Algorithm for MDP Model Checking?.
The package contains all original logfiles and the scripts that extract the relevant data from those logs to generate the plots as in the paper.
Furthermore, the artefact contains the exercised version of the model checking tool `Storm` with its dependencies and convenient installation scripts as well as all benchmark instances.
The user can thus replicate all experiments from the paper.
An appropriate subset of the experiments is given to allow a review in a timely manner. In addition, single experiments can be handpicked for replication.
This is a mild adaptation of the artefact for the paper "A Practitioner's Guide to MDP Model Checking Algorithms by Hartmanns et al. (TACAS'23)".This artefact was tested using the virtual machine (VM) for the TACAS'23 artefact evaluation, available at https://doi.org/10.5281/zenodo.7113222.
The VM is based on Ubuntu 22.04. Use the root password `tacas23`.
Other Linux and MacOS systems should work as well
Verification of multi-objective Markov models
No full textProbabilistic systems evolve based on environmental events that occur with a certain probability. For such systems to perform well, we are often interested in multiple objectives, i.e., quantitative performance measures like the probability of a failure or the expected time until task completion. Sometimes, these objectives conflict with each other: minimizing the failure probability possibly means completing the task takes longer. Compromises need to be found. We consider Markov models---particularly Markov decision processes (MDPs) and Markov Automata (MAs). These state-based modeling formalisms describe a system in its random environment. Starting from an initial state, the transitioning behavior in MDPs is determined by probabilistic and nondeterministic choices. MAs further extend MDPs by exponentially distributed continuous time delays. Rewards can be attached to states or transitions to model system quantities such as energy consumption, productivity, or monetary costs. Objectives are formally specified by a mapping from (infinite) system executions to the value of interest, e.g., the total accumulated costs or the average energy consumption. The expected value of an objective is defined once the nondeterminism is resolved using a strategy---intuitively reflecting the choices of a system controller. Different strategies induce different expected objective values. Multi-objective verification of MDPs and MAs analyzes the interplay between the considered objectives and identifies which trade-offs between expected objective values are possible, i.e., achievable by some strategy. We study practically efficient methods to compute the set of achievable solutions. For this, we establish a general framework and its instantiation for (undiscounted) total reachability reward objectives, long-run average reward objectives, and reward-bounded objectives. We propagate the errors made by approximative methods, yielding sound under- and over-approximations. We further consider multi-dimensional quantiles that ask under which reward constraints a given objective value is achievable. Finally, we investigate a setting in which the strategies must be simple, i.e., non-randomized and with limited memory access. All presented approaches are integrated into the state-of-the-art probabilistic model checker Storm. An extensive evaluation of this implementation on a broad set of multi-objective benchmarks shows that our approaches scale to large models with millions of states
- …
