Tuesday's talk: Pritam Roy on Magnifying Lens Abstraction
Luca de Alfaro
Speaker : Pritam Roy
E2 Rm. 398 (The "software engineering lab")
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 (MLA), 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, MLA 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 on three case
studies illustrating that MLA can provide accurate answers, with
savings in memory requirements.