Bi-Weekly Talk: Jip Spel: Are Parametric Markov Chains Monotonic?

Wednesday, July 24, 2019, 10:30am

Location: RWTH Aachen University, Department of Computer Science - Ahornstr. 55, building E3, room 9u10

Speaker: Jip Spel

 

Abstract:

We present 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.