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 . We formalise probabilistic refinement of action systems  in order to provide just such a front end, and we illustrate with the probabilistic model checker PRISM  how it can be used to reduce state explosion. The case study is based on a performance analysis of randomised backoff in wireless communication .