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...

• Type: Conference
• Year: 2008
• Where: QEST
• Authors: Pritam Roy, David Parker, Gethin Norman, Luca de Alfaro
• Keywords: Markov Decision, QEST 2008, Quantitative Evaluation Of Systems, Santa Cruz, Symbolic Mla