Tuesday's talk: Pritam Roy on Magnifying Lens Abstraction

0 views
Skip to first unread message

Luca de Alfaro

unread,
Jun 4, 2007, 7:08:39 PM6/4/07
to UCSC CS Theory and Software
Magnifying Lens Abstraction in Markov Decision Processes
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.

Reply all
Reply to author
Forward
0 new messages