Sound value iteration
From MaRDI portal
Abstract: Computing reachability probabilities is at the heart of probabilistic model checking. All model checkers compute these probabilities in an iterative fashion using value iteration. This technique approximates a fixed point from below by determining reachability probabilities for an increasing number of steps. To avoid results that are significantly off, variants have recently been proposed that converge from both below and above. These procedures require starting values for both sides. We present an alternative that does not require the a priori computation of starting vectors and that converges faster on many benchmarks. The crux of our technique is to give tight and safe bounds - whose computation is cheap - on the reachability probabilities. Lifting this technique to expected rewards is trivial for both Markov chains and MDPs. Experimental results on a large set of benchmarks show its scalability and efficiency.
Recommendations
Cited in
(22)- Of cores: a partial-exploration framework for Markov decision processes
- Comparison of algorithms for simple stochastic games
- Latticed \(k\)-induction with an application to probabilistic programs
- Comparison of algorithms for simple stochastic games
- Learning algorithms for verification of Markov decision processes
- Reachability in MDPs: refining convergence of value iteration
- Optimistic and topological value iteration for simple stochastic games
- On the Complexity of Value Iteration
- Ensuring the reliability of your model checker: interval iteration for Markov decision processes
- Optimistic value iteration
- Of cores: a partial-exploration framework for Markov decision processes
- Multi-objective optimization of long-run average and total rewards
- Multi-cost bounded tradeoff analysis in MDP
- Verification of multiplayer stochastic games via abstract dependency graphs
- Computing expected visiting times and stationary distributions in Markov chains: fast and accurate
- Value Iteration
- A practitioner's guide to MDP model checking algorithms
- Exploiting adjoints in property directed reachability analysis
- Correct probabilistic model checking with floating-point arithmetic
- Certificates for probabilistic pushdown automata via optimistic value iteration
- Under-approximating expected total rewards in POMDPs
- Probabilistic program verification via inductive synthesis of inductive invariants
This page was built for publication: Sound value iteration
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6041136)
