Magnifying-Lens Abstraction for Markov Decision Processes

ng-Lens Abstraction for Markov Decision Processes⋆ In Proc. of CAV 2007: 19th International Conference on Computer-Aided Verification, Lectures Notes in Computer Science. c Springer-Verlag, 2007. Luca de Alfaro and Pritam Roy Computer Engineering Department University of California, Santa Cruz, USA We present a novel abstraction technique which allows the analysis of reachability and safety properties of Markov decision processes with very large aces. 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 ding across the abstraction a magnifying lens which allowed viewing the concrete states. The algorithm adaptively refines the regions, using smaller regio...

• Type: Conference
• Year: 2007
• Where: CAV
• Authors: Luca de Alfaro, Pritam Roy
• Keywords: Abstraction, CAV 2007, Formal Methods, Lower Bounds, Markov Decision