Are Parametric Markov Chains Monotonic?

TL;DR

This paper introduces an efficient algorithm to verify the monotonicity of reachability probabilities in parametric Markov chains, leveraging graph structure and local transitions, significantly improving parameter synthesis speed.

Contribution

It presents a simple, graph-based algorithm that checks a sufficient condition for monotonicity, enabling faster parameter synthesis in parametric Markov chains.

Findings

Monotonicity can be automatically detected in several benchmarks.

The approach can accelerate parameter synthesis by up to orders of magnitude.

The algorithm uses only the graph structure and local transition probabilities.

Abstract

This paper presents a simple algorithm to check whether reachability probabilities in parametric Markov chains are monotonic in (some of) the parameters. The idea is to construct - only using the graph structure of the Markov chain and local transition probabilities - a pre-order on the states. Our algorithm cheaply checks a sufficient condition for monotonicity. Experiments show that monotonicity in several benchmarks is automatically detected, and monotonicity can speed up parameter synthesis up to orders of magnitude faster than a symbolic baseline.