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 | |
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