1 citations · 1 across the 2 of their papers we have counts for
6 papers
Multi-objective Optimization of Long-run Average and Total Rewards
Tim Quatmann, Joost-Pieter Katoen
This paper presents an efficient procedure for multi-objective model checking of long-run average reward (aka: mean pay-off) and total reward objectives as well as their combinatio…
Verification of indefinite-horizon POMDPs
Alexander Bork, Sebastian Junges, Joost-Pieter Katoen +1
The verification problem in MDPs asks whether, for any policy resolving the nondeterminism, the probability that something bad happens is bounded by some given threshold. This veri…
The Probabilistic Model Checker Storm
Christian Hensel, Sebastian Junges, Joost-Pieter Katoen +2
We present the probabilistic model checker Storm. Storm supports the analysis of discrete- and continuous-time variants of both Markov chains and Markov decision processes. Storm h…
Simple Strategies in Multi-Objective MDPs (Technical Report)
Florent Delgrange, Joost-Pieter Katoen, Tim Quatmann +1
We consider the verification of multiple expected reward objectives at once on Markov decision processes (MDPs). This enables a trade-off analysis among multiple objectives by obta…
Sound Value Iteration
Tim Quatmann, Joost-Pieter Katoen
Computing reachability probabilities is at the heart of probabilistic model checking. All model checkers compute these probabilities in an iterative fashion using value iteration.…
Markov Automata with Multiple Objectives
Tim Quatmann, Sebastian Junges, Joost-Pieter Katoen
Markov automata combine non-determinism, probabilistic branching, and exponentially distributed delays. This compositional variant of continuous-time Markov decision processes is u…