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

DOI10.1007/978-3-319-24953-7_10zbMATH Open1471.68144arXiv1504.02861OpenAlexW3104074232MaRDI QIDQ3460552FDOQ3460552

Publication date: 8 January 2016

Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1504.02861

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (4)

This page was built for publication: Explicit Model Checking of Very Large MDP Using Partitioning and Secondary Storage

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3460552)