Explicit Model Checking of Very Large MDP using Partitioning and Secondary Storage

TL;DR

This paper introduces a novel approach for probabilistic model checking of large Markov decision processes by leveraging secondary storage with partitioning and block-iterative algorithms, enabling analysis of models with billions of states.

Contribution

It presents a new technique combining partitioned state space exploration with secondary storage and a sparse matrix representation for efficient probabilistic analysis.

Findings

Successfully analyzed models with up to 3.5 billion states

Neutralized state space explosion in time-bounded property analysis

Implemented in the Modest Toolset with competitive performance

Abstract

The applicability of model checking is hindered by the state space explosion problem in combination with limited amounts of main memory. To extend its reach, the large available capacities of secondary storage such as hard disks can be exploited. Due to the specific performance characteristics of secondary storage technologies, specialised algorithms are required. In this paper, we present a technique to use secondary storage for probabilistic model checking of Markov decision processes. It combines state space exploration based on partitioning with a block-iterative variant of value iteration over the same partitions for the analysis of probabilistic reachability and expected-reward properties. A sparse matrix-like representation is used to store partitions on secondary storage in a compact format. All file accesses are sequential, and compression can be used without affecting runtime. The technique has been implemented within the Modest Toolset. We evaluate its performance on several benchmark models of up to 3.5 billion states. In the analysis of time-bounded properties on real-time models, our method neutralises the state space explosion induced by the time bound in its entirety.