A game-based abstraction-refinement framework for Markov decision processes
In the field of model checking, abstraction refinement has proved to be an extremely successful methodology for combating the state-space explosion problem. However, little practical progress has been made in the setting of probabilistic verification. In this paper we present a novel abstraction-ref...
| Main Authors: | , , , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
2010
|
| _version_ | 1826262619370029056 |
|---|---|
| author | Kattenbelt, M Kwiatkowska, M Norman, G Parker, D |
| author_facet | Kattenbelt, M Kwiatkowska, M Norman, G Parker, D |
| author_sort | Kattenbelt, M |
| collection | OXFORD |
| description | In the field of model checking, abstraction refinement has proved to be an extremely successful methodology for combating the state-space explosion problem. However, little practical progress has been made in the setting of probabilistic verification. In this paper we present a novel abstraction-refinement framework for Markov decision processes (MDPs), which are widely used for modelling and verifying systems that exhibit both probabilistic and nondeterministic behaviour. Our framework comprises an abstraction approach based on stochastic two-player games, two refinement methods and an efficient algorithm for an abstraction-refinement loop. The key idea behind the abstraction approach is to maintain a separation between nondeterminism present in the original MDP and nondeterminism introduced during the abstraction process, each type being represented by a different player in the game. Crucially, this allows lower and upper bounds to be computed for the values of reachability properties of the MDP. These give a quantitative measure of the quality of the abstraction and form the basis of the corresponding refinement methods. We describe a prototype implementation of our framework and present experimental results demonstrating automatic generation of compact, yet precise, abstractions for a large selection of real-world case studies. © 2010 Springer Science+Business Media, LLC. |
| first_indexed | 2024-03-06T19:39:05Z |
| format | Journal article |
| id | oxford-uuid:20096601-7c72-4999-bfca-6c31217dc24f |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-06T19:39:05Z |
| publishDate | 2010 |
| record_format | dspace |
| spelling | oxford-uuid:20096601-7c72-4999-bfca-6c31217dc24f2022-03-26T11:25:20ZA game-based abstraction-refinement framework for Markov decision processesJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:20096601-7c72-4999-bfca-6c31217dc24fEnglishSymplectic Elements at Oxford2010Kattenbelt, MKwiatkowska, MNorman, GParker, DIn the field of model checking, abstraction refinement has proved to be an extremely successful methodology for combating the state-space explosion problem. However, little practical progress has been made in the setting of probabilistic verification. In this paper we present a novel abstraction-refinement framework for Markov decision processes (MDPs), which are widely used for modelling and verifying systems that exhibit both probabilistic and nondeterministic behaviour. Our framework comprises an abstraction approach based on stochastic two-player games, two refinement methods and an efficient algorithm for an abstraction-refinement loop. The key idea behind the abstraction approach is to maintain a separation between nondeterminism present in the original MDP and nondeterminism introduced during the abstraction process, each type being represented by a different player in the game. Crucially, this allows lower and upper bounds to be computed for the values of reachability properties of the MDP. These give a quantitative measure of the quality of the abstraction and form the basis of the corresponding refinement methods. We describe a prototype implementation of our framework and present experimental results demonstrating automatic generation of compact, yet precise, abstractions for a large selection of real-world case studies. © 2010 Springer Science+Business Media, LLC. |
| spellingShingle | Kattenbelt, M Kwiatkowska, M Norman, G Parker, D A game-based abstraction-refinement framework for Markov decision processes |
| title | A game-based abstraction-refinement framework for Markov decision processes |
| title_full | A game-based abstraction-refinement framework for Markov decision processes |
| title_fullStr | A game-based abstraction-refinement framework for Markov decision processes |
| title_full_unstemmed | A game-based abstraction-refinement framework for Markov decision processes |
| title_short | A game-based abstraction-refinement framework for Markov decision processes |
| title_sort | game based abstraction refinement framework for markov decision processes |
| work_keys_str_mv | AT kattenbeltm agamebasedabstractionrefinementframeworkformarkovdecisionprocesses AT kwiatkowskam agamebasedabstractionrefinementframeworkformarkovdecisionprocesses AT normang agamebasedabstractionrefinementframeworkformarkovdecisionprocesses AT parkerd agamebasedabstractionrefinementframeworkformarkovdecisionprocesses AT kattenbeltm gamebasedabstractionrefinementframeworkformarkovdecisionprocesses AT kwiatkowskam gamebasedabstractionrefinementframeworkformarkovdecisionprocesses AT normang gamebasedabstractionrefinementframeworkformarkovdecisionprocesses AT parkerd gamebasedabstractionrefinementframeworkformarkovdecisionprocesses |