Efficient Formally Verified Maximal End Component Decomposition for MDPs

Arnd Hartmanns; Bram Kohlen; Peter Lammich

doi:10.1007/978-3-031-71162-6_11

Efficient Formally Verified Maximal End Component Decomposition for MDPs

Arnd Hartmanns, Bram Kohlen, Peter Lammich

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

16 Downloads (Pure)

Abstract

Identifying a Markov decision process’s maximal end components is a prerequisite for applying sound probabilistic model checking algorithms. In this paper, we present the first mechanized correctness proof of a maximal end component decomposition algorithm, which is an important algorithm in model checking, using the Isabelle/HOL theorem prover. We iteratively refine the high-level algorithm and proof into an imperative LLVM bytecode implementation that we integrate into the Modest Toolset ’s existing mcsta model checker. We bring the benefits of interactive theorem proving into practice by reducing the trusted code base of a popular probabilistic model checker and we experimentally show that our new verified maximal end component decomposition in mcsta performs on par with the tool’s previous unverified implementation.

Original language	English
Title of host publication	Formal methods
Subtitle of host publication	26th International Symposium, FM 2024 Milan, Italy, September 9-13, 2024. Proceedings, Part I
Editors	André Platzer, Kristin Yvonne Rozier, Matteo Pradella, Matteo Rossi
Publisher	Springer
Pages	206-225
Number of pages	20
ISBN (Electronic)	978-3-031-71162-6
ISBN (Print)	978-3-031-71161-9
DOIs	https://doi.org/10.1007/978-3-031-71162-6_11
Publication status	Published - 11 Sept 2024
Event	26th International Symposium on Formal Methods - Milan, Italy Duration: 11 Sept 2024 → 13 Sept 2024

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	14933
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	26th International Symposium on Formal Methods
Abbreviated title	FM 2024
Country/Territory	Italy
City	Milan
Period	11/09/24 → 13/09/24

Keywords

This work was part of the MISSION (Models in Space Systems: Integration, Operation, and Networking) project, funded by the European Union’s Horizon 2020 research and innovation programme under Marie Skłodowska-Curie Actions grant number 101008233.

Access to Document

10.1007/978-3-031-71162-6_11Licence: CC BY

Efficient Formally Verified Maximal End Component Decomposition for MDPsFinal published version, 680 KBLicence: CC BY

Cite this

Hartmanns, A., Kohlen, B., & Lammich, P. (2024). Efficient Formally Verified Maximal End Component Decomposition for MDPs. In A. Platzer, K. Y. Rozier, M. Pradella, & M. Rossi (Eds.), Formal methods: 26th International Symposium, FM 2024 Milan, Italy, September 9-13, 2024. Proceedings, Part I (pp. 206-225). (Lecture Notes in Computer Science; Vol. 14933). Springer. https://doi.org/10.1007/978-3-031-71162-6_11

Hartmanns, Arnd ; Kohlen, Bram ; Lammich, Peter. / Efficient Formally Verified Maximal End Component Decomposition for MDPs. Formal methods: 26th International Symposium, FM 2024 Milan, Italy, September 9-13, 2024. Proceedings, Part I. editor / André Platzer ; Kristin Yvonne Rozier ; Matteo Pradella ; Matteo Rossi. Springer, 2024. pp. 206-225 (Lecture Notes in Computer Science).

@inproceedings{2d4997fa59694d19ad66840ef997dbcd,

title = "Efficient Formally Verified Maximal End Component Decomposition for MDPs",

abstract = "Identifying a Markov decision process{\textquoteright}s maximal end components is a prerequisite for applying sound probabilistic model checking algorithms. In this paper, we present the first mechanized correctness proof of a maximal end component decomposition algorithm, which is an important algorithm in model checking, using the Isabelle/HOL theorem prover. We iteratively refine the high-level algorithm and proof into an imperative LLVM bytecode implementation that we integrate into the Modest Toolset {\textquoteright}s existing mcsta model checker. We bring the benefits of interactive theorem proving into practice by reducing the trusted code base of a popular probabilistic model checker and we experimentally show that our new verified maximal end component decomposition in mcsta performs on par with the tool{\textquoteright}s previous unverified implementation.",

keywords = "This work was part of the MISSION (Models in Space Systems: Integration, Operation, and Networking) project, funded by the European Union{\textquoteright}s Horizon 2020 research and innovation programme under Marie Sk{\l}odowska-Curie Actions grant number 101008233.",

author = "Arnd Hartmanns and Bram Kohlen and Peter Lammich",

year = "2024",

month = sep,

day = "11",

doi = "10.1007/978-3-031-71162-6_11",

language = "English",

isbn = "978-3-031-71161-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "206--225",

editor = "Andr{\'e} Platzer and Rozier, {Kristin Yvonne} and Matteo Pradella and Matteo Rossi",

booktitle = "Formal methods",

address = "Germany",

note = "26th International Symposium on Formal Methods, FM 2024 ; Conference date: 11-09-2024 Through 13-09-2024",

}

Hartmanns, A, Kohlen, B & Lammich, P 2024, Efficient Formally Verified Maximal End Component Decomposition for MDPs. in A Platzer, KY Rozier, M Pradella & M Rossi (eds), Formal methods: 26th International Symposium, FM 2024 Milan, Italy, September 9-13, 2024. Proceedings, Part I. Lecture Notes in Computer Science, vol. 14933, Springer, pp. 206-225, 26th International Symposium on Formal Methods, Milan, Italy, 11/09/24. https://doi.org/10.1007/978-3-031-71162-6_11

Efficient Formally Verified Maximal End Component Decomposition for MDPs. / Hartmanns, Arnd; Kohlen, Bram; Lammich, Peter.
Formal methods: 26th International Symposium, FM 2024 Milan, Italy, September 9-13, 2024. Proceedings, Part I. ed. / André Platzer; Kristin Yvonne Rozier; Matteo Pradella; Matteo Rossi. Springer, 2024. p. 206-225 (Lecture Notes in Computer Science; Vol. 14933).

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

TY - GEN

T1 - Efficient Formally Verified Maximal End Component Decomposition for MDPs

AU - Hartmanns, Arnd

AU - Kohlen, Bram

AU - Lammich, Peter

PY - 2024/9/11

Y1 - 2024/9/11

N2 - Identifying a Markov decision process’s maximal end components is a prerequisite for applying sound probabilistic model checking algorithms. In this paper, we present the first mechanized correctness proof of a maximal end component decomposition algorithm, which is an important algorithm in model checking, using the Isabelle/HOL theorem prover. We iteratively refine the high-level algorithm and proof into an imperative LLVM bytecode implementation that we integrate into the Modest Toolset ’s existing mcsta model checker. We bring the benefits of interactive theorem proving into practice by reducing the trusted code base of a popular probabilistic model checker and we experimentally show that our new verified maximal end component decomposition in mcsta performs on par with the tool’s previous unverified implementation.

AB - Identifying a Markov decision process’s maximal end components is a prerequisite for applying sound probabilistic model checking algorithms. In this paper, we present the first mechanized correctness proof of a maximal end component decomposition algorithm, which is an important algorithm in model checking, using the Isabelle/HOL theorem prover. We iteratively refine the high-level algorithm and proof into an imperative LLVM bytecode implementation that we integrate into the Modest Toolset ’s existing mcsta model checker. We bring the benefits of interactive theorem proving into practice by reducing the trusted code base of a popular probabilistic model checker and we experimentally show that our new verified maximal end component decomposition in mcsta performs on par with the tool’s previous unverified implementation.

KW - This work was part of the MISSION (Models in Space Systems: Integration, Operation, and Networking) project, funded by the European Union’s Horizon 2020 research and innovation programme under Marie Skłodowska-Curie Actions grant number 101008233.

UR - http://www.scopus.com/inward/record.url?scp=85204631824&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-71162-6_11

DO - 10.1007/978-3-031-71162-6_11

M3 - Conference contribution

SN - 978-3-031-71161-9

T3 - Lecture Notes in Computer Science

SP - 206

EP - 225

BT - Formal methods

A2 - Platzer, André

A2 - Rozier, Kristin Yvonne

A2 - Pradella, Matteo

A2 - Rossi, Matteo

PB - Springer

T2 - 26th International Symposium on Formal Methods

Y2 - 11 September 2024 through 13 September 2024

ER -

Hartmanns A, Kohlen B, Lammich P. Efficient Formally Verified Maximal End Component Decomposition for MDPs. In Platzer A, Rozier KY, Pradella M, Rossi M, editors, Formal methods: 26th International Symposium, FM 2024 Milan, Italy, September 9-13, 2024. Proceedings, Part I. Springer. 2024. p. 206-225. (Lecture Notes in Computer Science). doi: 10.1007/978-3-031-71162-6_11

Efficient Formally Verified Maximal End Component Decomposition for MDPs

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Artifact for the paper "Efficient Formally Verified Maximal End Component Decomposition for MDPs"

Cite this

Efficient Formally Verified Maximal End Component Decomposition for MDPs

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Datasets

Artifact for the paper "Efficient Formally Verified Maximal End Component Decomposition for MDPs"

Cite this