Symbolic Model Checking of Weighted PCTL Using Dependency Graphs

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

2 Citationer (Scopus)

Resumé

We present a global and local algorithm for model checking a weighted variant of PCTL with upper-bound weight constraints, on probabilistic weighted Kripke structures where the weights are vectors with non-zero magnitude. Both algorithms under- and over approximate a fixed-point over a symbolic dependency graph, until sufficient evidence to prove or disprove the given formula is found. Fixed-point computations are carried out in the domain of (multidimensional) probabilistic step functions, encoded as interval decision diagrams. The global algorithm works similarly to classic value iteration for PCTL in that it evaluates all nodes of the dependency graph iteratively, while the local algorithm performs a search-like evaluation of the given dependency graph in an attempt to find enough evidence locally to prove/disprove a given formula, without having to evaluate all nodes. Both algorithms are evaluated on several experiments and we show that the local algorithm generally outperforms the global algorithm.
OriginalsprogEngelsk
TitelNASA Formal Methods - 11th International Symposium, NFM 2019, Proceedings
RedaktørerKristin Yvonne Rozier, Julia M. Badger
Antal sider18
ForlagSpringer
Publikationsdato2019
Sider298-315
ISBN (Trykt)978-3-030-20651-2
ISBN (Elektronisk)978-3-030-20652-9
DOI
StatusUdgivet - 2019
BegivenhedNFM19: 11th Annual NASA Formal Methods Symposium: Challenges for Future Exploration - Rice University, Houston, USA
Varighed: 7 maj 20199 maj 2019
Konferencens nummer: 11
https://robonaut.jsc.nasa.gov/R2/pages/nfm2019.html

Konference

KonferenceNFM19: 11th Annual NASA Formal Methods Symposium
Nummer11
LokationRice University
LandUSA
ByHouston
Periode07/05/201909/05/2019
Internetadresse
NavnLecture Notes in Computer Science
Vol/bind11460
ISSN0302-9743

Fingerprint

Model checking

Citer dette

Jensen, M. C., Mariegaard, A., & Larsen, K. G. (2019). Symbolic Model Checking of Weighted PCTL Using Dependency Graphs. I K. Y. Rozier, & J. M. Badger (red.), NASA Formal Methods - 11th International Symposium, NFM 2019, Proceedings (s. 298-315). Springer. Lecture Notes in Computer Science, Bind. 11460 https://doi.org/10.1007/978-3-030-20652-9_20
Jensen, Mathias Claus ; Mariegaard, Anders ; Larsen, Kim Guldstrand. / Symbolic Model Checking of Weighted PCTL Using Dependency Graphs. NASA Formal Methods - 11th International Symposium, NFM 2019, Proceedings. red. / Kristin Yvonne Rozier ; Julia M. Badger. Springer, 2019. s. 298-315 (Lecture Notes in Computer Science, Bind 11460).
@inproceedings{deaf6232e834467fb5ebfc73d1c6c970,
title = "Symbolic Model Checking of Weighted PCTL Using Dependency Graphs",
abstract = "We present a global and local algorithm for model checking a weighted variant of PCTL with upper-bound weight constraints, on probabilistic weighted Kripke structures where the weights are vectors with non-zero magnitude. Both algorithms under- and over approximate a fixed-point over a symbolic dependency graph, until sufficient evidence to prove or disprove the given formula is found. Fixed-point computations are carried out in the domain of (multidimensional) probabilistic step functions, encoded as interval decision diagrams. The global algorithm works similarly to classic value iteration for PCTL in that it evaluates all nodes of the dependency graph iteratively, while the local algorithm performs a search-like evaluation of the given dependency graph in an attempt to find enough evidence locally to prove/disprove a given formula, without having to evaluate all nodes. Both algorithms are evaluated on several experiments and we show that the local algorithm generally outperforms the global algorithm.",
keywords = "Model Checking, Dependency graph, probabilistic CTL, On-the-fly methods",
author = "Jensen, {Mathias Claus} and Anders Mariegaard and Larsen, {Kim Guldstrand}",
year = "2019",
doi = "10.1007/978-3-030-20652-9_20",
language = "English",
isbn = "978-3-030-20651-2",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "298--315",
editor = "Rozier, {Kristin Yvonne} and Badger, {Julia M.}",
booktitle = "NASA Formal Methods - 11th International Symposium, NFM 2019, Proceedings",
address = "Germany",

}

Jensen, MC, Mariegaard, A & Larsen, KG 2019, Symbolic Model Checking of Weighted PCTL Using Dependency Graphs. i KY Rozier & JM Badger (red), NASA Formal Methods - 11th International Symposium, NFM 2019, Proceedings. Springer, Lecture Notes in Computer Science, bind 11460, s. 298-315, NFM19: 11th Annual NASA Formal Methods Symposium, Houston, USA, 07/05/2019. https://doi.org/10.1007/978-3-030-20652-9_20

Symbolic Model Checking of Weighted PCTL Using Dependency Graphs. / Jensen, Mathias Claus; Mariegaard, Anders; Larsen, Kim Guldstrand.

NASA Formal Methods - 11th International Symposium, NFM 2019, Proceedings. red. / Kristin Yvonne Rozier; Julia M. Badger. Springer, 2019. s. 298-315 (Lecture Notes in Computer Science, Bind 11460).

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

TY - GEN

T1 - Symbolic Model Checking of Weighted PCTL Using Dependency Graphs

AU - Jensen, Mathias Claus

AU - Mariegaard, Anders

AU - Larsen, Kim Guldstrand

PY - 2019

Y1 - 2019

N2 - We present a global and local algorithm for model checking a weighted variant of PCTL with upper-bound weight constraints, on probabilistic weighted Kripke structures where the weights are vectors with non-zero magnitude. Both algorithms under- and over approximate a fixed-point over a symbolic dependency graph, until sufficient evidence to prove or disprove the given formula is found. Fixed-point computations are carried out in the domain of (multidimensional) probabilistic step functions, encoded as interval decision diagrams. The global algorithm works similarly to classic value iteration for PCTL in that it evaluates all nodes of the dependency graph iteratively, while the local algorithm performs a search-like evaluation of the given dependency graph in an attempt to find enough evidence locally to prove/disprove a given formula, without having to evaluate all nodes. Both algorithms are evaluated on several experiments and we show that the local algorithm generally outperforms the global algorithm.

AB - We present a global and local algorithm for model checking a weighted variant of PCTL with upper-bound weight constraints, on probabilistic weighted Kripke structures where the weights are vectors with non-zero magnitude. Both algorithms under- and over approximate a fixed-point over a symbolic dependency graph, until sufficient evidence to prove or disprove the given formula is found. Fixed-point computations are carried out in the domain of (multidimensional) probabilistic step functions, encoded as interval decision diagrams. The global algorithm works similarly to classic value iteration for PCTL in that it evaluates all nodes of the dependency graph iteratively, while the local algorithm performs a search-like evaluation of the given dependency graph in an attempt to find enough evidence locally to prove/disprove a given formula, without having to evaluate all nodes. Both algorithms are evaluated on several experiments and we show that the local algorithm generally outperforms the global algorithm.

KW - Model Checking

KW - Dependency graph

KW - probabilistic CTL

KW - On-the-fly methods

U2 - 10.1007/978-3-030-20652-9_20

DO - 10.1007/978-3-030-20652-9_20

M3 - Article in proceeding

SN - 978-3-030-20651-2

T3 - Lecture Notes in Computer Science

SP - 298

EP - 315

BT - NASA Formal Methods - 11th International Symposium, NFM 2019, Proceedings

A2 - Rozier, Kristin Yvonne

A2 - Badger, Julia M.

PB - Springer

ER -

Jensen MC, Mariegaard A, Larsen KG. Symbolic Model Checking of Weighted PCTL Using Dependency Graphs. I Rozier KY, Badger JM, red., NASA Formal Methods - 11th International Symposium, NFM 2019, Proceedings. Springer. 2019. s. 298-315. (Lecture Notes in Computer Science, Bind 11460). https://doi.org/10.1007/978-3-030-20652-9_20