Smart Sampling for Lightweight Verification of Markov Decision Processes

TL;DR

This paper introduces smart sampling algorithms that significantly improve the efficiency of verifying Markov decision processes by better exploring scheduler space, enhancing Monte Carlo verification techniques.

Contribution

The paper presents novel smart sampling algorithms that outperform simple sampling methods in finding optimal schedulers for MDP verification.

Findings

Smart sampling algorithms outperform simple sampling in efficiency.

Enhanced performance in verifying MDPs with Monte Carlo methods.

Significant reduction in computational resources needed for scheduler optimization.

Abstract

Markov decision processes (MDP) are useful to model optimisation problems in concurrent systems. To verify MDPs with efficient Monte Carlo techniques requires that their nondeterminism be resolved by a scheduler. Recent work has introduced the elements of lightweight techniques to sample directly from scheduler space, but finding optimal schedulers by simple sampling may be inefficient. Here we describe "smart" sampling algorithms that can make substantial improvements in performance.