Efficient Algorithms for Time- and Cost-Bounded Probabilistic Model Checking

TL;DR

This paper introduces three novel algorithms for efficiently model-checking time- and cost-bounded properties in probabilistic systems, avoiding state space explosion and enabling analysis at any cost bound.

Contribution

The authors present three new algorithms that avoid unfolding in probabilistic timed systems, improving efficiency and scalability for bounded property verification.

Findings

Algorithms outperform traditional unfolding methods

Able to compute results for any cost bound efficiently

Implementation validated on multiple case studies

Abstract

In the design of probabilistic timed systems, bounded requirements concerning behaviour that occurs within a given time, energy, or more generally cost budget are of central importance. Traditionally, such requirements have been model-checked via a reduction to the unbounded case by unfolding the model according to the cost bound. This exacerbates the state space explosion problem and significantly increases runtime. In this paper, we present three new algorithms to model-check time- and cost-bounded properties for Markov decision processes and probabilistic timed automata that avoid unfolding. They are based on a modified value iteration process, on an enumeration of schedulers, and on state elimination techniques. We can now obtain results for any cost bound on a single state space no larger than for the corresponding unbounded or expected-value property. In particular, we can naturally compute the cumulative distribution function at no overhead. We evaluate the applicability and compare the performance of our new algorithms and their implementation on a number of case studies from the literature.