UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

Optimistic Value Iteration

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). Green open access

[img]
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 > 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.ucl.ac.uk/id/eprint/10097745
Downloads since deposit
13Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item