Sciweavers

Share
QEST
2008
IEEE

Symbolic Magnifying Lens Abstraction in Markov Decision Processes

9 years 4 months ago
Symbolic Magnifying Lens Abstraction in Markov Decision Processes
Magnifying Lens Abstraction in Markov Decision Processes ∗ Pritam Roy1 David Parker2 Gethin Norman2 Luca de Alfaro1 Computer Engineering Dept, UC Santa Cruz, Santa Cruz, CA, USA 1 Oxford University Computing Laboratory, Oxford, UK 2 May 2008 Technical Report No. UCSC-SOE-08-05 School of Engineering, University of California, Santa Cruz, CA, USA paper, we combine abstraction-refinement and symbolic techniques to fight the state-space explosion problem when cking Markov Decision Processes (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 states. To compute such bounds, MLA iterates over the regions, analysing the concrete states of each region in turn - as if one was sliding a magnifying lens across the system to view the states. The algorithm adaptively refines the regions, using smaller regions where mor...
Pritam Roy, David Parker, Gethin Norman, Luca de A
Added 01 Jun 2010
Updated 01 Jun 2010
Type Conference
Year 2008
Where QEST
Authors Pritam Roy, David Parker, Gethin Norman, Luca de Alfaro
Comments (0)
books