@inproceedings{8431a24b277e4154ad611700bd602d2f,
title = "Quantitative refinement and model checking for the analysis of probabilistic systems",
abstract = "For standard (ie non-probabilistic) systems of reasonable size, correctness is analysed by simulation and/or model checking, possibly with standard program-logical arguments beforehand to reduce the problem size by abstraction. For probabilistic systems there are model checkers and simulators too; but probabilistic program logics are rarer. Thus e.g. model checkers face more severe exposure to state explosion because {"}front-end{"} probabilistic abstraction techniques are not so widely known [18]. We formalise probabilistic refinement of action systems [3] in order to provide just such a front end, and we illustrate with the probabilistic model checker PRISM [21] how it can be used to reduce state explosion. The case study is based on a performance analysis of randomised backoff in wireless communication [1].",
author = "McIver, {A. K.}",
year = "2006",
doi = "10.1007/11813040_10",
language = "English",
isbn = "3540372156",
volume = "4085 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer, Springer Nature",
pages = "131--146",
editor = "Jayadev Misra and Tobias Nipkow and Emil Sekerinski",
booktitle = "FM 2006: Formal Methods - 14th International Symposium on Formal Methods, Proceedings",
address = "United States",
}