Abstraction Framework for Markov Decision Processes and PCTL via Games
Markov decision processes (MDPs) are natural models of computation in a wide range of applications. Probabilistic computation tree logic (PCTL) is a powerful temporal logic for reasoning about and verifying such models. Often, these models are prohibitively large or infinite-state, and so direct mod...
| Main Authors: | , |
|---|---|
| Format: | Report |
| Published: |
Oxford University Computing Laboratory
2009
|
| _version_ | 1826291840954925056 |
|---|---|
| author | Kattenbelt, M Huth, M |
| author_facet | Kattenbelt, M Huth, M |
| author_sort | Kattenbelt, M |
| collection | OXFORD |
| description | Markov decision processes (MDPs) are natural models of computation in a wide range of applications. Probabilistic computation tree logic (PCTL) is a powerful temporal logic for reasoning about and verifying such models. Often, these models are prohibitively large or infinite-state, and so direct model checking of PCTL formulae over MDPs is infeasible. A recognised solution to this problem would be to develop finite-state abstractions of MDPs that soundly abstract the satisfaction of arbitrary PCTL formulae over very large or infinite-state MDPs. We state requirements for such an abstraction framework ? e.g. that model checking of abstractions underapproximates generalised model checking for PCTL ? and show important metaproperties that follow from these requirements. We take a notion of stochastic games from stochastic reachability analysis, adapt it, develop a simulation order for these adapted games ? decidable in P ? and prove that this adaptation meets all key requirements for an abstraction framework. Unlike generalised model checking, model checking our abstractions is reasonably efficient. We also show that the refinement characterised by PCTL is coarser than our simulation order. |
| first_indexed | 2024-03-07T03:05:31Z |
| format | Report |
| id | oxford-uuid:b260fd27-e74b-4485-b461-d8988ab8ad68 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T03:05:31Z |
| publishDate | 2009 |
| publisher | Oxford University Computing Laboratory |
| record_format | dspace |
| spelling | oxford-uuid:b260fd27-e74b-4485-b461-d8988ab8ad682022-03-27T04:11:20ZAbstraction Framework for Markov Decision Processes and PCTL via GamesReporthttp://purl.org/coar/resource_type/c_93fcuuid:b260fd27-e74b-4485-b461-d8988ab8ad68Department of Computer ScienceOxford University Computing Laboratory2009Kattenbelt, MHuth, MMarkov decision processes (MDPs) are natural models of computation in a wide range of applications. Probabilistic computation tree logic (PCTL) is a powerful temporal logic for reasoning about and verifying such models. Often, these models are prohibitively large or infinite-state, and so direct model checking of PCTL formulae over MDPs is infeasible. A recognised solution to this problem would be to develop finite-state abstractions of MDPs that soundly abstract the satisfaction of arbitrary PCTL formulae over very large or infinite-state MDPs. We state requirements for such an abstraction framework ? e.g. that model checking of abstractions underapproximates generalised model checking for PCTL ? and show important metaproperties that follow from these requirements. We take a notion of stochastic games from stochastic reachability analysis, adapt it, develop a simulation order for these adapted games ? decidable in P ? and prove that this adaptation meets all key requirements for an abstraction framework. Unlike generalised model checking, model checking our abstractions is reasonably efficient. We also show that the refinement characterised by PCTL is coarser than our simulation order. |
| spellingShingle | Kattenbelt, M Huth, M Abstraction Framework for Markov Decision Processes and PCTL via Games |
| title | Abstraction Framework for Markov Decision Processes and PCTL via Games |
| title_full | Abstraction Framework for Markov Decision Processes and PCTL via Games |
| title_fullStr | Abstraction Framework for Markov Decision Processes and PCTL via Games |
| title_full_unstemmed | Abstraction Framework for Markov Decision Processes and PCTL via Games |
| title_short | Abstraction Framework for Markov Decision Processes and PCTL via Games |
| title_sort | abstraction framework for markov decision processes and pctl via games |
| work_keys_str_mv | AT kattenbeltm abstractionframeworkformarkovdecisionprocessesandpctlviagames AT huthm abstractionframeworkformarkovdecisionprocessesandpctlviagames |