Reduction and Refinement Strategies for Probabilistic Analysis

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

doi:10.1007/3-540-45605-8_5

Reduction and Refinement Strategies for Probabilistic Analysis

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

56 Citations (Scopus)

Abstract

We report on new strategies for model checking quantitative reachability properties of Markov decision processes by successive refinements. In our approach, properties are analyzed on abstractions rather than directly on the given model. Such abstractions are expected to be 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 involved in settling the validity of the property is more costly than the refinement process, the method profits from applying such numerical analysis on smaller state spaces. The method is significantly enhanced by a number of novel strategies: a strategy for reducing the size of the numerical problems to be analyzed by identification of so-called essential states, and heuristic strategies for guiding the refinement process.

Original language	English
Title of host publication	Process Algebra and Probabilistic Methods: Performance Modeling and Verification
Subtitle of host publication	Second Joint International Workshop PAPM-PROBMIV 2002, Copenhagen, Denmark, July 25-26, 2002 Proceedings
Editors	Holger Hermanns, Roberto Segala
Place of Publication	Berlin, Heidelberg
Publisher	Springer
Pages	57-76
Number of pages	20
ISBN (Electronic)	978-3-540-45605-6
ISBN (Print)	978-3-540-43913-4
DOIs	https://doi.org/10.1007/3-540-45605-8_5
Publication status	Published - 2002
Externally published	Yes
Event	2nd International Workshop on Process Algebra and Probabilistic Methods & Probabilistic Methods in Verification, PAPM-PROBMIV 2002 - Copenhagen, Denmark Duration: 25 Jul 2002 → 26 Jul 2002 Conference number: 2

Publication series

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

Workshop

Workshop	2nd International Workshop on Process Algebra and Probabilistic Methods & Probabilistic Methods in Verification, PAPM-PROBMIV 2002
Abbreviated title	PAPM-PROBMIV
Country/Territory	Denmark
City	Copenhagen
Period	25/07/02 → 26/07/02

Keywords

n/a OA procedure

Access to Document

10.1007/3-540-45605-8_5

Cite this

d' Argenio, P. R., Jeannet, B., Jensen, H. E., & Larsen, K. G. (2002). Reduction and Refinement Strategies for Probabilistic Analysis. In H. Hermanns, & R. Segala (Eds.), Process Algebra and Probabilistic Methods: Performance Modeling and Verification: Second Joint International Workshop PAPM-PROBMIV 2002, Copenhagen, Denmark, July 25-26, 2002 Proceedings (pp. 57-76). (Lecture Notes in Computer Science; Vol. 2399). Springer. https://doi.org/10.1007/3-540-45605-8_5

d' Argenio, Pedro R. ; Jeannet, Bertrand ; Jensen, Henrik E. et al. / Reduction and Refinement Strategies for Probabilistic Analysis. Process Algebra and Probabilistic Methods: Performance Modeling and Verification: Second Joint International Workshop PAPM-PROBMIV 2002, Copenhagen, Denmark, July 25-26, 2002 Proceedings. editor / Holger Hermanns ; Roberto Segala. Berlin, Heidelberg : Springer, 2002. pp. 57-76 (Lecture Notes in Computer Science).

@inproceedings{43f15fd6ff0546f694efd10cc84261d1,

title = "Reduction and Refinement Strategies for Probabilistic Analysis",

abstract = "We report on new strategies for model checking quantitative reachability properties of Markov decision processes by successive refinements. In our approach, properties are analyzed on abstractions rather than directly on the given model. Such abstractions are expected to be 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 involved in settling the validity of the property is more costly than the refinement process, the method profits from applying such numerical analysis on smaller state spaces. The method is significantly enhanced by a number of novel strategies: a strategy for reducing the size of the numerical problems to be analyzed by identification of so-called essential states, and heuristic strategies for guiding the refinement process.",

keywords = "n/a OA procedure",

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

year = "2002",

doi = "10.1007/3-540-45605-8_5",

language = "English",

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

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "57--76",

editor = "Holger Hermanns and Roberto Segala",

booktitle = "Process Algebra and Probabilistic Methods: Performance Modeling and Verification",

address = "Germany",

note = "2nd International Workshop on Process Algebra and Probabilistic Methods & Probabilistic Methods in Verification, PAPM-PROBMIV 2002 , PAPM-PROBMIV ; Conference date: 25-07-2002 Through 26-07-2002",

}

d' Argenio, PR, Jeannet, B, Jensen, HE & Larsen, KG 2002, Reduction and Refinement Strategies for Probabilistic Analysis. in H Hermanns & R Segala (eds), Process Algebra and Probabilistic Methods: Performance Modeling and Verification: Second Joint International Workshop PAPM-PROBMIV 2002, Copenhagen, Denmark, July 25-26, 2002 Proceedings. Lecture Notes in Computer Science, vol. 2399, Springer, Berlin, Heidelberg, pp. 57-76, 2nd International Workshop on Process Algebra and Probabilistic Methods & Probabilistic Methods in Verification, PAPM-PROBMIV 2002 , Copenhagen, Denmark, 25/07/02. https://doi.org/10.1007/3-540-45605-8_5

Reduction and Refinement Strategies for Probabilistic Analysis. / d' Argenio, Pedro R.; Jeannet, Bertrand; Jensen, Henrik E. et al.
Process Algebra and Probabilistic Methods: Performance Modeling and Verification: Second Joint International Workshop PAPM-PROBMIV 2002, Copenhagen, Denmark, July 25-26, 2002 Proceedings. ed. / Holger Hermanns; Roberto Segala. Berlin, Heidelberg: Springer, 2002. p. 57-76 (Lecture Notes in Computer Science; Vol. 2399).

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

TY - GEN

T1 - Reduction and Refinement Strategies for Probabilistic Analysis

AU - d' Argenio, Pedro R.

AU - Jeannet, Bertrand

AU - Jensen, Henrik E.

AU - Larsen, Kim G.

N1 - Conference code: 2

PY - 2002

Y1 - 2002

N2 - We report on new strategies for model checking quantitative reachability properties of Markov decision processes by successive refinements. In our approach, properties are analyzed on abstractions rather than directly on the given model. Such abstractions are expected to be 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 involved in settling the validity of the property is more costly than the refinement process, the method profits from applying such numerical analysis on smaller state spaces. The method is significantly enhanced by a number of novel strategies: a strategy for reducing the size of the numerical problems to be analyzed by identification of so-called essential states, and heuristic strategies for guiding the refinement process.

AB - We report on new strategies for model checking quantitative reachability properties of Markov decision processes by successive refinements. In our approach, properties are analyzed on abstractions rather than directly on the given model. Such abstractions are expected to be 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 involved in settling the validity of the property is more costly than the refinement process, the method profits from applying such numerical analysis on smaller state spaces. The method is significantly enhanced by a number of novel strategies: a strategy for reducing the size of the numerical problems to be analyzed by identification of so-called essential states, and heuristic strategies for guiding the refinement process.

KW - n/a OA procedure

U2 - 10.1007/3-540-45605-8_5

DO - 10.1007/3-540-45605-8_5

M3 - Conference contribution

SN - 978-3-540-43913-4

T3 - Lecture Notes in Computer Science

SP - 57

EP - 76

BT - Process Algebra and Probabilistic Methods: Performance Modeling and Verification

A2 - Hermanns, Holger

A2 - Segala, Roberto

PB - Springer

CY - Berlin, Heidelberg

T2 - 2nd International Workshop on Process Algebra and Probabilistic Methods & Probabilistic Methods in Verification, PAPM-PROBMIV 2002

Y2 - 25 July 2002 through 26 July 2002

ER -

d' Argenio PR, Jeannet B, Jensen HE, Larsen KG. Reduction and Refinement Strategies for Probabilistic Analysis. In Hermanns H, Segala R, editors, Process Algebra and Probabilistic Methods: Performance Modeling and Verification: Second Joint International Workshop PAPM-PROBMIV 2002, Copenhagen, Denmark, July 25-26, 2002 Proceedings. Berlin, Heidelberg: Springer. 2002. p. 57-76. (Lecture Notes in Computer Science). doi: 10.1007/3-540-45605-8_5

Reduction and Refinement Strategies for Probabilistic Analysis

Abstract

Publication series

Workshop

Keywords

Access to Document

Fingerprint

Cite this