Extending Stochastic Model Checking with Path Rewards | Han Yue
| | Abstract | Stochastic modeling is widely used for design and analysis of systems in various application domains. Stochastic model checking is an automatic procedure validating whether a stochastic model satisfi es a given property which is normally expressed by some temporal logics. One of the state of art model checking tools is PRISM. In the project, Model Checking Real Life, conducted during the spring of 2012, a hypothetic ambulance system has been introduced and some PRISM Discrete-time Markov Chain (DTMC) models have been developed based on this system. We also attempted to evaluate some Probabilistic Computation Tree Logic (PCTL) like formulae with path reward properties over these models. However, PRISM only supports state rewards formulae which validate the expected rewards based on a certain set of paths start from a specific state. After some further studies, we believe the concept of path reward properties is also useful to the analyses of other systems.
In order to fulfill this purpose, in this paper, PCTL with state reward formulae is formally extended with path reward formulae as PCTLR. Base on the concept of dynamic programming, algorithms for model checking PCTLR probability path reward formulae over both DTMCs and Markov Decision Processes (MDP) with rewards are developed. Besides, PRISM is extended to support all the above concepts. While PCTLR is incorporated into the PRISM property specification language, we also feel the need to grant PRISM with more flexibility, in this project, an extended filter with "cust" operator is designed and implemented for the extended PRISM. Finally, the extended PRISM is tested from three aspects: correctness, performance and robustness. | | Type | Master's thesis [Academic thesis] | | Year | 2013 | | Publisher | Technical University of Denmark, Department of Applied Mathematics and Computer Science | | Address | Matematiktorvet, Building 303B, DK-2800 Kgs. Lyngby, Denmark, compute@compute.dtu.dk | | Note | DTU supervisor: Flemming Nielson, fnie@dtu.dk, DTU Compute | | Electronic version(s) | [pdf] | | Publication link | http://www.compute.dtu.dk/English.aspx | | BibTeX data | [bibtex] | | IMM Group(s) | Computer Science & Engineering |
|