Optimistic Value Iteration

Arnd Hartmanns; Benjamin Lucien Kaminski

doi:10.1007/978-3-030-53291-8_26

Optimistic Value Iteration

Arnd Hartmanns^*, Benjamin Lucien Kaminski

^*Corresponding author for this work

Formal Methods and Tools

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

35 Citations (Scopus)

96 Downloads (Pure)

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.

Original language	English
Title of host publication	Computer Aided Verification
Subtitle of host publication	32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21–24, 2020, Proceedings, Part II
Editors	Shuvendu K. Lahiri, Chao Wang
Publisher	Springer
Pages	488-511
Number of pages	24
ISBN (Electronic)	978-3-030-53291-8
ISBN (Print)	978-3-030-53290-1
DOIs	https://doi.org/10.1007/978-3-030-53291-8_26
Publication status	Published - 14 Jul 2020
Event	32nd International Conference on Computer-Aided Verification, CAV 2020 - Virtual Conference, Los Angeles, United States Duration: 19 Jul 2020 → 24 Jul 2020 Conference number: 32 http://i-cav.org/2020/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	12225

Conference

Conference	32nd International Conference on Computer-Aided Verification, CAV 2020
Abbreviated title	CAV 2020
Country/Territory	United States
City	Los Angeles
Period	19/07/20 → 24/07/20
Internet address	http://i-cav.org/2020/

Access to Document

10.1007/978-3-030-53291-8_26Licence: CC BY

Hartmanns-Kaminski2020_Chapter_OptimisticValueIterationFinal published version, 973 KBLicence: CC BY

Cite this

@inproceedings{9c5c329bd54f42ddac234df52cee5b4b,

title = "Optimistic Value Iteration",

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{\textquoteright}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{\textquoteright}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.",

author = "Arnd Hartmanns and Kaminski, {Benjamin Lucien}",

note = "Funding Information: The authors are listed alphabetically. This work was partly performed while author B. L. Kaminski was at RWTH Aachen University, Aachen, Germany. This work was supported by ERC Advanced Grant 787914 (FRAPPANT), DFG Research Training Group 2236 (UnRAVeL), and NWO VENI grant no. 639.021.754.. Acknowledgments. The authors thank Tim Quatmann (RWTH Aachen) for fruitful discussions when the idea of OVI initially came up in late 2018, and for his help in implementing and optimising the SVI implementation in mcsta. Publisher Copyright: {\textcopyright} 2020, The Author(s).; 32nd International Conference on Computer-Aided Verification, CAV 2020, CAV 2020 ; Conference date: 19-07-2020 Through 24-07-2020",

year = "2020",

month = jul,

day = "14",

doi = "10.1007/978-3-030-53291-8_26",

language = "English",

isbn = "978-3-030-53290-1",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "488--511",

editor = "Lahiri, {Shuvendu K.} and Chao Wang",

booktitle = "Computer Aided Verification",

address = "Germany",

url = "http://i-cav.org/2020/",

}

Hartmanns, A & Kaminski, BL 2020, Optimistic Value Iteration. in SK Lahiri & C Wang (eds), Computer Aided Verification: 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21–24, 2020, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12225, Springer, pp. 488-511, 32nd International Conference on Computer-Aided Verification, CAV 2020, Los Angeles, California, United States, 19/07/20. https://doi.org/10.1007/978-3-030-53291-8_26

Optimistic Value Iteration. / Hartmanns, Arnd; Kaminski, Benjamin Lucien.
Computer Aided Verification: 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21–24, 2020, Proceedings, Part II. ed. / Shuvendu K. Lahiri; Chao Wang. Springer, 2020. p. 488-511 (Lecture Notes in Computer Science; Vol. 12225).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Optimistic Value Iteration

AU - Hartmanns, Arnd

AU - Kaminski, Benjamin Lucien

N1 - Conference code: 32

PY - 2020/7/14

Y1 - 2020/7/14

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-030-53291-8_26

DO - 10.1007/978-3-030-53291-8_26

M3 - Conference contribution

SN - 978-3-030-53290-1

T3 - Lecture Notes in Computer Science

SP - 488

EP - 511

BT - Computer Aided Verification

A2 - Lahiri, Shuvendu K.

A2 - Wang, Chao

PB - Springer

T2 - 32nd International Conference on Computer-Aided Verification, CAV 2020

Y2 - 19 July 2020 through 24 July 2020

ER -

Optimistic Value Iteration

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this