L. de Alfaro, P. Roy.
Magnifying-Lens Abstraction for Markov Decision Processes.
Technical report ucsc-crl-06-15, School of Engineering,
University of California, Santa Cruz, 2006.
Abstract
Postscript
PDF
Abstract
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.