# 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.

## Key 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.

---
Source: https://tomesphere.com/paper/1907.08491