by Friedrich Gretz, Joost-Pieter Katoen, Annabelle McIver
Reference:
Operational versus weakest pre-expectation semantics for the probabilistic guarded command language (Friedrich Gretz, Joost-Pieter Katoen, Annabelle McIver), In Performance Evaluation, volume 73, 2014. (Special Issue on the 9th International Conference on Quantitative Evaluation of Systems)
Bibtex Entry:
@article{Gretz2014110, title = "Operational versus weakest pre-expectation semantics for the probabilistic guarded command language ", journal = "Performance Evaluation ", volume = "73", number = "0", pages = "110 - 132", year = "2014", note = "Special Issue on the 9th International Conference on Quantitative Evaluation of Systems ", issn = "0166-5316", doi = "http://dx.doi.org/10.1016/j.peva.2013.11.004", url = "http://www.sciencedirect.com/science/article/pii/S0166531613001429", author = "Friedrich Gretz and Joost-Pieter Katoen and Annabelle McIver", keywords = "Expectation transformer semantics", keywords = "Operational semantics", keywords = "Markov decision process", keywords = "Expected rewards " }