Continuous-Time Markov Decisions based on Partial Exploration

TL;DR

This paper introduces a framework that accelerates time-bounded reachability analysis of continuous-time Markov decision processes by focusing on small, representative subsystems identified through simulations, leading to significant speed improvements.

Contribution

It presents a novel subsystem-based approach for Markov decision process analysis, combining simulation-guided selection with iterative enlargement, and demonstrates substantial efficiency gains.

Findings

Orders-of-magnitude speed-ups in analysis time

Effective subsystem identification through simulations

Versatile framework applicable to multiple algorithms

Abstract

We provide a framework for speeding up algorithms for time-bounded reachability analysis of continuous-time Markov decision processes. The principle is to find a small, but almost equivalent subsystem of the original system and only analyse the subsystem. Candidates for the subsystem are identified through simulations and iteratively enlarged until runs are represented in the subsystem with high enough probability. The framework is thus dual to that of abstraction refinement. We instantiate the framework in several ways with several traditional algorithms and experimentally confirm orders-of-magnitude speed ups in many cases.