Exploiting robust optimization for interval probabilistic bisimulation

Ernst Moritz Hahn; Vahid Hashemi; Holger Hermanns; Andrea Turrini

doi:10.1007/978-3-319-43425-4_4

Exploiting robust optimization for interval probabilistic bisimulation

Ernst Moritz Hahn, Vahid Hashemi^*, Holger Hermanns, Andrea Turrini

^*Corresponding author for this work

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

5 Citations (Scopus)

Abstract

Verification of PCTL properties of MDPs with convex uncertainties has been investigated recently by Puggelli et al. However, model checking algorithms typically suffer from the state space explosion problem. In this paper, we discuss the use of probabilistic bisimulation to reduce the size of such an MDP while preserving the PCTL properties it satisfies. As a core part, we show that deciding bisimilarity of a pair of states can be encoded as adjustable robust counterpart of an uncertain LP. We show that using affine decision rules, probabilistic bisimulation relation can be approximated in polynomial time. We have implemented our approach and demonstrate its effectiveness on several case studies.

Original language	English
Title of host publication	Quantitative Evaluation of Systems
Subtitle of host publication	13th International Conference, QEST 2016, Quebec City, QC, Canada, August 23-25, 2016, Proceedings
Editors	Benny Van Houdt, Gul Agha
Place of Publication	Cham
Publisher	Springer
Pages	55-71
Number of pages	17
ISBN (Electronic)	978-3-319-43425-4
ISBN (Print)	978-3-319-43424-7
DOIs	https://doi.org/10.1007/978-3-319-43425-4_4
Publication status	Published - 2016
Externally published	Yes
Event	13th International Conference on Quantitative Evaluation of Systems, QEST 2016 - Hôtel Château Laurier, Quebec City, Canada Duration: 23 Aug 2016 → 25 Aug 2016 Conference number: 13

Publication series

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

Conference

Conference	13th International Conference on Quantitative Evaluation of Systems, QEST 2016
Abbreviated title	QEST 2016
Country/Territory	Canada
City	Quebec City
Period	23/08/16 → 25/08/16

Keywords

Linear programming problem
Robust optimization
Uncertain data
Robust counterpart
Computational tractability

Access to Document

10.1007/978-3-319-43425-4_4

Cite this

Hahn, E. M., Hashemi, V., Hermanns, H., & Turrini, A. (2016). Exploiting robust optimization for interval probabilistic bisimulation. In B. Van Houdt, & G. Agha (Eds.), Quantitative Evaluation of Systems: 13th International Conference, QEST 2016, Quebec City, QC, Canada, August 23-25, 2016, Proceedings (pp. 55-71). (Lecture Notes in Computer Science; Vol. 9826). Springer. https://doi.org/10.1007/978-3-319-43425-4_4

Hahn, Ernst Moritz ; Hashemi, Vahid ; Hermanns, Holger et al. / Exploiting robust optimization for interval probabilistic bisimulation. Quantitative Evaluation of Systems: 13th International Conference, QEST 2016, Quebec City, QC, Canada, August 23-25, 2016, Proceedings. editor / Benny Van Houdt ; Gul Agha. Cham : Springer, 2016. pp. 55-71 (Lecture Notes in Computer Science).

@inproceedings{e4a5646fa5c64f1397e4873796fa7483,

title = "Exploiting robust optimization for interval probabilistic bisimulation",

abstract = "Verification of PCTL properties of MDPs with convex uncertainties has been investigated recently by Puggelli et al. However, model checking algorithms typically suffer from the state space explosion problem. In this paper, we discuss the use of probabilistic bisimulation to reduce the size of such an MDP while preserving the PCTL properties it satisfies. As a core part, we show that deciding bisimilarity of a pair of states can be encoded as adjustable robust counterpart of an uncertain LP. We show that using affine decision rules, probabilistic bisimulation relation can be approximated in polynomial time. We have implemented our approach and demonstrate its effectiveness on several case studies.",

keywords = "Linear programming problem, Robust optimization, Uncertain data, Robust counterpart, Computational tractability",

author = "Hahn, {Ernst Moritz} and Vahid Hashemi and Holger Hermanns and Andrea Turrini",

year = "2016",

doi = "10.1007/978-3-319-43425-4_4",

language = "English",

isbn = "978-3-319-43424-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "55--71",

editor = "{Van Houdt}, Benny and Gul Agha",

booktitle = "Quantitative Evaluation of Systems",

address = "Germany",

note = "13th International Conference on Quantitative Evaluation of Systems, QEST 2016, QEST 2016 ; Conference date: 23-08-2016 Through 25-08-2016",

}

Hahn, EM, Hashemi, V, Hermanns, H & Turrini, A 2016, Exploiting robust optimization for interval probabilistic bisimulation. in B Van Houdt & G Agha (eds), Quantitative Evaluation of Systems: 13th International Conference, QEST 2016, Quebec City, QC, Canada, August 23-25, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9826, Springer, Cham, pp. 55-71, 13th International Conference on Quantitative Evaluation of Systems, QEST 2016, Quebec City, Quebec, Canada, 23/08/16. https://doi.org/10.1007/978-3-319-43425-4_4

Exploiting robust optimization for interval probabilistic bisimulation. / Hahn, Ernst Moritz; Hashemi, Vahid; Hermanns, Holger et al.
Quantitative Evaluation of Systems: 13th International Conference, QEST 2016, Quebec City, QC, Canada, August 23-25, 2016, Proceedings. ed. / Benny Van Houdt; Gul Agha. Cham: Springer, 2016. p. 55-71 (Lecture Notes in Computer Science; Vol. 9826).

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

TY - GEN

T1 - Exploiting robust optimization for interval probabilistic bisimulation

AU - Hahn, Ernst Moritz

AU - Hashemi, Vahid

AU - Hermanns, Holger

AU - Turrini, Andrea

N1 - Conference code: 13

PY - 2016

Y1 - 2016

N2 - Verification of PCTL properties of MDPs with convex uncertainties has been investigated recently by Puggelli et al. However, model checking algorithms typically suffer from the state space explosion problem. In this paper, we discuss the use of probabilistic bisimulation to reduce the size of such an MDP while preserving the PCTL properties it satisfies. As a core part, we show that deciding bisimilarity of a pair of states can be encoded as adjustable robust counterpart of an uncertain LP. We show that using affine decision rules, probabilistic bisimulation relation can be approximated in polynomial time. We have implemented our approach and demonstrate its effectiveness on several case studies.

AB - Verification of PCTL properties of MDPs with convex uncertainties has been investigated recently by Puggelli et al. However, model checking algorithms typically suffer from the state space explosion problem. In this paper, we discuss the use of probabilistic bisimulation to reduce the size of such an MDP while preserving the PCTL properties it satisfies. As a core part, we show that deciding bisimilarity of a pair of states can be encoded as adjustable robust counterpart of an uncertain LP. We show that using affine decision rules, probabilistic bisimulation relation can be approximated in polynomial time. We have implemented our approach and demonstrate its effectiveness on several case studies.

KW - Linear programming problem

KW - Robust optimization

KW - Uncertain data

KW - Robust counterpart

KW - Computational tractability

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

U2 - 10.1007/978-3-319-43425-4_4

DO - 10.1007/978-3-319-43425-4_4

M3 - Conference contribution

SN - 978-3-319-43424-7

T3 - Lecture Notes in Computer Science

SP - 55

EP - 71

BT - Quantitative Evaluation of Systems

A2 - Van Houdt, Benny

A2 - Agha, Gul

PB - Springer

CY - Cham

T2 - 13th International Conference on Quantitative Evaluation of Systems, QEST 2016

Y2 - 23 August 2016 through 25 August 2016

ER -

Hahn EM, Hashemi V, Hermanns H, Turrini A. Exploiting robust optimization for interval probabilistic bisimulation. In Van Houdt B, Agha G, editors, Quantitative Evaluation of Systems: 13th International Conference, QEST 2016, Quebec City, QC, Canada, August 23-25, 2016, Proceedings. Cham: Springer. 2016. p. 55-71. (Lecture Notes in Computer Science). doi: 10.1007/978-3-319-43425-4_4

Exploiting robust optimization for interval probabilistic bisimulation

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this