L.: Symbolic magnifying lens abstraction in Markov decision processes

In this paper, we combine abstraction-refinement and symbolic techniques to fight the state-space explosion problem when model checking Markov Decision Pro-cesses (MDPs). The abstract-refinement technique, called magnifying-lens abstraction (MLA), partitions the state-space into regions and computes upper and lower bounds for reachability and safety properties on the regions, rather than the states. To compute such bounds, MLA iterates over the regions, analysing the concrete states of each re-gion in turn- as if one was sliding a magnifying lens across the system to view the states. The algorithm adaptively re-fines the regions, using smaller regions where more detail is required, until the difference between the bounds is be-low a specified accuracy. The symbolic technique is based on Multi-Terminal Binary Decision Diagrams (MTBDDs) which have been used extensively to provide compact en-codings of probabilistic models. We introduce a symbolic version of the MLA algorithm, called symbolic MLA, which combines the power of both practical techniques when ver-ifying MDPs. An implementation of symbolic MLA in the probabilistic model checker PRISM and experimental re-sults to illustrate the advantages of our approach are pre-sented.