کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
463055 | 696947 | 2014 | 23 صفحه PDF | دانلود رایگان |
This paper proposes a simple operational semantics of pGCL, Dijkstra’s guarded command language extended with probabilistic choice, and relates this to pGCL’s wp-semantics by McIver and Morgan. Parametric Markov decision processes whose state rewards depend on the post-expectation at hand are used as the operational model. We show that the weakest pre-expectation of a pGCL-program w.r.t. a post-expectation corresponds to the expected cumulative reward to reach a terminal state in the parametric MDP associated to the program. In a similar way, we show a correspondence between weakest liberal pre-expectations and liberal expected cumulative rewards. The verification of probabilistic programs using wp-semantics and operational semantics is illustrated using a simple running example.
Journal: Performance Evaluation - Volume 73, March 2014, Pages 110–132