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

Mittwoch, 24.07.2019, 10.30 Uhr

Ort: RWTH Aachen University, Informatikzentrum - Ahornstr. 55, Erweiterungsgebäude E3, Raum 9u10

Vortragende:  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.