Magnifying-Lens Abstraction for Markov Decision Processes

8 years 10 months ago
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...
Luca de Alfaro, Pritam Roy
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where CAV
Authors Luca de Alfaro, Pritam Roy
Comments (0)