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
(26)- Multi-objective optimization of long-run average and total rewards
- Comparison of algorithms for simple stochastic games
- Verification of multiplayer stochastic games via abstract dependency graphs
- Ensuring the reliability of your model checker: interval iteration for Markov decision processes
- Multi-cost bounded tradeoff analysis in MDP
- Optimistic value iteration
- Reachability in MDPs: refining convergence of value iteration
- Value Iteration
- Comparison of algorithms for simple stochastic games
- On the Complexity of Value Iteration
- Of cores: a partial-exploration framework for Markov decision processes
- Of cores: a partial-exploration framework for Markov decision processes
- Optimistic and topological value iteration for simple stochastic games
- A practitioner's guide to MDP model checking algorithms
- Exploiting adjoints in property directed reachability analysis
- Under-approximating expected total rewards in POMDPs
- Correct probabilistic model checking with floating-point arithmetic
- Certificates for probabilistic pushdown automata via optimistic value iteration
- Probabilistic program verification via inductive synthesis of inductive invariants
- Computing expected visiting times and stationary distributions in Markov chains: fast and accurate
- Learning algorithms for verification of Markov decision processes
- On piecewise affine reachability with Bellman operators
- A direct reduction from stochastic parity games to simple stochastic games
- Expectation in stochastic games with prefix-independent objectives
- Adjointness in property directed reachability analysis
- Latticed \(k\)-induction with an application to probabilistic programs
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)
