Report icon

Report

Abstraction Framework for Markov Decision Processes and PCTL via Games

Abstract:

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

Expand abstract

Actions


Access Document


Files:

Authors


Mark Kattenbelt More by this author
Michael Huth More by this author
Publisher:
Oxford University Computing Laboratory
Publication date:
2009
URN:
uuid:b260fd27-e74b-4485-b461-d8988ab8ad68
Local pid:
cs:2964

Terms of use


Metrics



If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP