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
|