Hartmanns, A;
Kaminski, BL;
(2020)
Optimistic Value Iteration.
In:
International Conference on Computer Aided Verification CAV 2020: Computer Aided Verification.
(pp. pp. 488-511).
Springer: Los Angeles, CA, USA (online).
Preview |
Text
Kaminski_Hartmanns-Kaminski2020_Chapter_OptimisticValueIteration.pdf - Published Version Download (996kB) | Preview |
Abstract
Markov decision processes are widely used for planning and verification in settings that combine controllable or adversarial choices with probabilistic behaviour. The standard analysis algorithm, value iteration, only provides lower bounds on infinite-horizon probabilities and rewards. Two “sound” variations, which also deliver an upper bound, have recently appeared. In this paper, we present a new sound approach that leverages value iteration’s ability to usually deliver good lower bounds: we obtain a lower bound via standard value iteration, use the result to “guess” an upper bound, and prove the latter’s correctness. We present this optimistic value iteration approach for computing reachability probabilities as well as expected rewards. It is easy to implement and performs well, as we show via an extensive experimental evaluation using our implementation within the mcsta model checker of the Modest Toolset.
| Type: | Proceedings paper |
|---|---|
| Title: | Optimistic Value Iteration |
| Event: | 32nd International Conference on Computer-Aided Verification (CAV 2020) |
| Location: | online |
| Dates: | 21 July 2020 - 24 July 2020 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/978-3-030-53291-8_26 |
| Publisher version: | https://doi.org/10.1007/978-3-030-53291-8_26 |
| Language: | English |
| Additional information: | This is an open access article under the CC BY license (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited. |
| Keywords: | probabilistic model checking, Markov decision processes, value iteration, quantitative verification |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery-pp.ucl.ac.uk/id/eprint/10097745 |
Archive Staff Only
 |
View Item |
