Reachability Analysis of Probabilistic Systems by Successive Refinements

Pedro R. d' Argenio; Bertrand Jeannet; Henrik E. Jensen; Kim G. Larsen

doi:10.1007/3-540-44804-7_3

Reachability Analysis of Probabilistic Systems by Successive Refinements

Pedro R. d' Argenio, Bertrand Jeannet, Henrik E. Jensen, Kim G. Larsen

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

114 Citations (Scopus)

3 Downloads (Pure)

Abstract

We report on a novel development to model check quantitative reachability properties on Markov decision processes together with its prototype implementation. The innovation of the technique is that the analysis is performed on an abstraction of the model under analysis. Such an abstraction is significantly smaller than the original model and may safely refute or accept the required property. Otherwise, the abstraction is refined and the process repeated. As the numerical analysis necessary to determine the validity of the property is more costly than the refinement process, the technique profits from applying such numerical analysis on smaller state spaces.

Original language	English
Title of host publication	Process Algebra and Probabilistic Methods. Performance Modelling and Verification
Subtitle of host publication	Joint International Workshop, PAPM-PROBMIV 2001 Aachen, Germany, September 12–14, 2001 Proceedings
Place of Publication	Berlin, Heidelberg
Publisher	Springer
Pages	39-56
ISBN (Electronic)	978-3-540-44804-4
ISBN (Print)	978-3-540-42556-4
DOIs	https://doi.org/10.1007/3-540-44804-7_3
Publication status	Published - 2001
Event	Joint International Workshop on Process Algebra and Probabilistic Methods & Probabilistic Methods in Verification, PAPM-PROBMIV 2001 - Aachen, Germany Duration: 12 Sept 2001 → 14 Sept 2001

Publication series

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

Workshop

Workshop	Joint International Workshop on Process Algebra and Probabilistic Methods & Probabilistic Methods in Verification, PAPM-PROBMIV 2001
Abbreviated title	PAPM-PROBMIV
Country/Territory	Germany
City	Aachen
Period	12/09/01 → 14/09/01

Keywords

n/a OA procedure

Access to Document

10.1007/3-540-44804-7_3

Cite this

d' Argenio, P. R., Jeannet, B., Jensen, H. E., & Larsen, K. G. (2001). Reachability Analysis of Probabilistic Systems by Successive Refinements. In Process Algebra and Probabilistic Methods. Performance Modelling and Verification: Joint International Workshop, PAPM-PROBMIV 2001 Aachen, Germany, September 12–14, 2001 Proceedings (pp. 39-56). (Lecture Notes in Computer Science; Vol. 2165). Springer. https://doi.org/10.1007/3-540-44804-7_3

d' Argenio, Pedro R. ; Jeannet, Bertrand ; Jensen, Henrik E. et al. / Reachability Analysis of Probabilistic Systems by Successive Refinements. Process Algebra and Probabilistic Methods. Performance Modelling and Verification: Joint International Workshop, PAPM-PROBMIV 2001 Aachen, Germany, September 12–14, 2001 Proceedings. Berlin, Heidelberg : Springer, 2001. pp. 39-56 (Lecture Notes in Computer Science).

@inproceedings{095586ff509b42e39e564c50fb7585c8,

title = "Reachability Analysis of Probabilistic Systems by Successive Refinements",

abstract = "We report on a novel development to model check quantitative reachability properties on Markov decision processes together with its prototype implementation. The innovation of the technique is that the analysis is performed on an abstraction of the model under analysis. Such an abstraction is significantly smaller than the original model and may safely refute or accept the required property. Otherwise, the abstraction is refined and the process repeated. As the numerical analysis necessary to determine the validity of the property is more costly than the refinement process, the technique profits from applying such numerical analysis on smaller state spaces.",

keywords = "n/a OA procedure",

author = "{d' Argenio}, {Pedro R.} and Bertrand Jeannet and Jensen, {Henrik E.} and Larsen, {Kim G.}",

year = "2001",

doi = "10.1007/3-540-44804-7_3",

language = "English",

isbn = "978-3-540-42556-4",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "39--56",

booktitle = "Process Algebra and Probabilistic Methods. Performance Modelling and Verification",

note = "Joint International Workshop on Process Algebra and Probabilistic Methods & Probabilistic Methods in Verification, PAPM-PROBMIV 2001, PAPM-PROBMIV ; Conference date: 12-09-2001 Through 14-09-2001",

}

d' Argenio, PR, Jeannet, B, Jensen, HE & Larsen, KG 2001, Reachability Analysis of Probabilistic Systems by Successive Refinements. in Process Algebra and Probabilistic Methods. Performance Modelling and Verification: Joint International Workshop, PAPM-PROBMIV 2001 Aachen, Germany, September 12–14, 2001 Proceedings. Lecture Notes in Computer Science, vol. 2165, Springer, Berlin, Heidelberg, pp. 39-56, Joint International Workshop on Process Algebra and Probabilistic Methods & Probabilistic Methods in Verification, PAPM-PROBMIV 2001, Aachen, Germany, 12/09/01. https://doi.org/10.1007/3-540-44804-7_3

Reachability Analysis of Probabilistic Systems by Successive Refinements. / d' Argenio, Pedro R.; Jeannet, Bertrand; Jensen, Henrik E. et al.
Process Algebra and Probabilistic Methods. Performance Modelling and Verification: Joint International Workshop, PAPM-PROBMIV 2001 Aachen, Germany, September 12–14, 2001 Proceedings. Berlin, Heidelberg: Springer, 2001. p. 39-56 (Lecture Notes in Computer Science; Vol. 2165).

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

TY - GEN

T1 - Reachability Analysis of Probabilistic Systems by Successive Refinements

AU - d' Argenio, Pedro R.

AU - Jeannet, Bertrand

AU - Jensen, Henrik E.

AU - Larsen, Kim G.

PY - 2001

Y1 - 2001

N2 - We report on a novel development to model check quantitative reachability properties on Markov decision processes together with its prototype implementation. The innovation of the technique is that the analysis is performed on an abstraction of the model under analysis. Such an abstraction is significantly smaller than the original model and may safely refute or accept the required property. Otherwise, the abstraction is refined and the process repeated. As the numerical analysis necessary to determine the validity of the property is more costly than the refinement process, the technique profits from applying such numerical analysis on smaller state spaces.

AB - We report on a novel development to model check quantitative reachability properties on Markov decision processes together with its prototype implementation. The innovation of the technique is that the analysis is performed on an abstraction of the model under analysis. Such an abstraction is significantly smaller than the original model and may safely refute or accept the required property. Otherwise, the abstraction is refined and the process repeated. As the numerical analysis necessary to determine the validity of the property is more costly than the refinement process, the technique profits from applying such numerical analysis on smaller state spaces.

KW - n/a OA procedure

U2 - 10.1007/3-540-44804-7_3

DO - 10.1007/3-540-44804-7_3

M3 - Conference contribution

SN - 978-3-540-42556-4

T3 - Lecture Notes in Computer Science

SP - 39

EP - 56

BT - Process Algebra and Probabilistic Methods. Performance Modelling and Verification

PB - Springer

CY - Berlin, Heidelberg

T2 - Joint International Workshop on Process Algebra and Probabilistic Methods & Probabilistic Methods in Verification, PAPM-PROBMIV 2001

Y2 - 12 September 2001 through 14 September 2001

ER -

d' Argenio PR, Jeannet B, Jensen HE, Larsen KG. Reachability Analysis of Probabilistic Systems by Successive Refinements. In Process Algebra and Probabilistic Methods. Performance Modelling and Verification: Joint International Workshop, PAPM-PROBMIV 2001 Aachen, Germany, September 12–14, 2001 Proceedings. Berlin, Heidelberg: Springer. 2001. p. 39-56. (Lecture Notes in Computer Science). doi: 10.1007/3-540-44804-7_3