Luca de Alfaro and Pritam Roy
01/01/2006 09:00 AM
Computer Engineering
We present a novel abstraction technique which allows the analysis of reachability and safety properties of Markov decision processes with very large state spaces. The technique, called magnifying-lens abstraction, copes with the state-explosion problem by partitioning the state-space into regions, and by computing upper and lower bounds for reachability and safety properties on the regions, rather than on the states. To compute these bounds, magnifying-lens abstraction iterates over the regions, considering the concrete states of each region in turn, as if one were sliding across the abstraction a magnifying lens which allowed viewing the concrete states. The algorithm adaptively refines the regions, using smaller regions where more detail is needed, until the difference between upper and lower bounds is smaller than a specified accuracy. We provide experimental results illustrating that magnifying-lens abstractions can provide accurate answers, with drastic savings in memory requirements, in many cases where previous abstraction techniques yield no benefit.
