@MASTERSTHESIS\{IMM2013-06670,
    author       = "H. Yue",
    title        = "Extending Stochastic Model Checking with Path Rewards",
    year         = "2013",
    school       = "Technical University of Denmark, Department of Applied Mathematics and Computer Science",
    address      = "Matematiktorvet, Building 303B, {DK-}2800 Kgs. Lyngby, Denmark, compute@compute.dtu.dk",
    type         = "",
    note         = "{DTU} supervisor: Flemming Nielson, fnie@dtu.dk, {DTU} Compute",
    url          = "http://www.compute.dtu.dk/English.aspx",
    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 satisfies 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."
}